@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00198951,
 author = {青木, 善貴 and 小形, 真平},
 book = {ソフトウェアエンジニアリングシンポジウム2019論文集},
 month = {Aug},
 note = {FRAM (Functional Resonance Analysis Method : 機能共鳴分析手法) は複雑なシステムの機能の構成と機能間の相互作用をモデル化して分析する手法である．FRAM では，事故は機能間のパフォーマンスの予期せぬ変動の組み合わせ （機能共鳴） から生じ，このパフォーマンスの変動を監視し減衰させることによって防止できるとしている．しかしながら，FRAM モデルの分析は，分析者のドメイン知識に頼った定性的評価でなされ，定量的評価を行う方法は未確立である．そこで本研究では，分析者が FRAM モデルの振る舞いを理解することを支援する目的で，確率を扱えるモデル検査ツール PRISM によりモデルの振る舞いを数値化して表す手法を提案する．本稿では，提案手法を FRAM 分析の事例に適用して，数値化により振る舞いを理解しやすくできること示した．また，変動を想定したモデル修正による振る舞いの数値の変化を追うことにより，端的にパフォーマンスの変動を捉えることができた．, FRAM is a method to model and analyze the configuration of functions and the interaction between functions of complex systems. In FRAM, an accident results from a combination of unexpected fluctuations in performance between functions. It can be prevented by monitoring and attenuating this change in performance. However, the analysis of FRAM model is a qualitative evaluation that relies on the analyst's domain knowledge, and there is no established method for quantitative evaluation. So, in this research, in order to support the understanding of the behavior of FRAM model, we propose a method to represent the behavior of the model with the model inspection tool PRISM that can handle the probability. In this paper, we apply the proposed method to the case study of FRAM analysis and show that it is easy to understand the behavior by quantification. By comparing the numerical values of the verification results obtained by changing the model, it was possible to catch the fluctuation of the performance.},
 pages = {116--125},
 publisher = {情報処理学会},
 title = {確率的モデル検査器を用いたFRAMモデル理解の支援},
 volume = {2019},
 year = {2019}
}