情報制御システムのモデル検査における反例分析支援ツールの開発

• Item type: SIG Technical Reports(1)
• 公開日: 2014-03-12
• タイトル: 情報制御システムのモデル検査における反例分析支援ツールの開発
• タイトル / 言語: en
• タイトル: An Analysis Support Tool of Counterexamples for Model-Checking of ICS
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: モデル・形式手法
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 茨城大学
• 著者所属: 茨城大学
• 著者所属: 茨城工業高等専門学校
• 著者所属: 茨城大学
• 著者所属(英): en
• 著者所属(英): Ibaraki University
• 著者所属(英): en
• 著者所属(英): Ibaraki University
• 著者所属(英): en
• 著者所属(英): Ibaraki National College of Technology
• 著者所属(英): en
• 著者所属(英): Ibaraki University
• 著者名: 大森, 祐貴; 小山, 恭平; 小飼, 敬; 上田, 賀一
• 著者名(英): Yuki, Omorii; Kyohei, Oyama; Kei, Kogai; Yoshikazu, Ueda
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 情報制御システムを対象としたモデル検査は，安全性を確保する上で意味あるアプローチといえる．この際，任意の性質が満たされない実行系列 （反例） を得ることで不具合の原因特定に役立てることができる．しかし，反例を理解するには専門的な知識が必要となり，反例から振舞い仕様の問題箇所を特定するのは困難である．そこで本研究ではモデル検査ツールにおける反例分析支援のための可視化ツールを開発した．具体的な事例を適用しその結果，本ツールが問題箇所の特定において，有責な情報を提供できることがわかった．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Model checking for Information Control System is an effective approach in order to ensure safety. In this case, obtaining execution sequences not to satisfy properties(counterexample) is useful to find out cause of errors. However, we require expertise to understand the counterexample and it is difficult to identify error locations of behavior specification by the counterexample. Therefore, this study report about a visualizing tool which was developed to support analyzing counterexample on model checking tool SPIN. It found that developed tool can provide valuable information in identifying error locations.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2014-SE-183, 号 11, p. 1-8, 発行日 2014-03-12
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会