WEKO3
アイテム
確率的モデル検査器を用いたFRAMモデル理解の支援
https://ipsj.ixsq.nii.ac.jp/records/198951
https://ipsj.ixsq.nii.ac.jp/records/198951a26b97d2-36ae-43d2-a6ee-0b67cf4d4cce
名前 / ファイル | ライセンス | アクション |
---|---|---|
![]() |
Copyright (c) 2019 by the Information Processing Society of Japan
|
|
オープンアクセス |
Item type | Symposium(1) | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
公開日 | 2019-08-22 | |||||||||
タイトル | ||||||||||
タイトル | 確率的モデル検査器を用いたFRAMモデル理解の支援 | |||||||||
タイトル | ||||||||||
言語 | en | |||||||||
タイトル | Support of FRAM model understanding using a probabilistic model checker | |||||||||
言語 | ||||||||||
言語 | jpn | |||||||||
キーワード | ||||||||||
主題Scheme | Other | |||||||||
主題 | 形式手法,テスト | |||||||||
資源タイプ | ||||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||
資源タイプ | conference paper | |||||||||
著者所属 | ||||||||||
日本ユニシス株式会社 | ||||||||||
著者所属 | ||||||||||
信州大学 | ||||||||||
著者名 |
青木, 善貴
× 青木, 善貴
× 小形, 真平
|
|||||||||
論文抄録 | ||||||||||
内容記述タイプ | Other | |||||||||
内容記述 | FRAM (Functional Resonance Analysis Method : 機能共鳴分析手法) は複雑なシステムの機能の構成と機能間の相互作用をモデル化して分析する手法である.FRAM では,事故は機能間のパフォーマンスの予期せぬ変動の組み合わせ (機能共鳴) から生じ,このパフォーマンスの変動を監視し減衰させることによって防止できるとしている.しかしながら,FRAM モデルの分析は,分析者のドメイン知識に頼った定性的評価でなされ,定量的評価を行う方法は未確立である.そこで本研究では,分析者が FRAM モデルの振る舞いを理解することを支援する目的で,確率を扱えるモデル検査ツール PRISM によりモデルの振る舞いを数値化して表す手法を提案する.本稿では,提案手法を FRAM 分析の事例に適用して,数値化により振る舞いを理解しやすくできること示した.また,変動を想定したモデル修正による振る舞いの数値の変化を追うことにより,端的にパフォーマンスの変動を捉えることができた. | |||||||||
論文抄録(英) | ||||||||||
内容記述タイプ | Other | |||||||||
内容記述 | 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. | |||||||||
書誌情報 |
ソフトウェアエンジニアリングシンポジウム2019論文集 巻 2019, p. 116-125, 発行日 2019-08-22 |
|||||||||
出版者 | ||||||||||
言語 | ja | |||||||||
出版者 | 情報処理学会 |