文献

J-GLOBAL ID：201502221176836682   整理番号：15A0585785

モジュラ化手法によるモデル検査の検討とモジュラ検証の実用化

Investigation of model checking by modular approach, and practicality of modular verification

著者 (5件)： 宮島卓巳 (茨城大) ,  小飼敬 (茨城工高専) ,  上田賀一 (茨城大) ,  山形知行 (日立) ,  武澤隆之 (日立)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 114  号： 501(KBSE2014 52-64)  ページ： 25-30  発行年： 2015年02月26日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 検査対象を機械的かつ網羅的に探索するモデル検査は,探索範囲の指数的増加のため適用が困難である。そこで,検査対象を構造と振舞いの観点から結合度の低い箇所を分割することでモジュラ化を行い,別々に検証し,1回に探索する範囲を制限することでモデル検査の実用化を目指す。本研究では,列車運行システムにおいてモジュラ化の有無による実験結果を比較し,有効性を評価する。(著者抄録)

シソーラス用語： *モデル検査 ,  生産方式 ,  *モジュール構造 ,  *組合せ問題 ,  実用化 ,  挙動 ,  強度 ,  分割 ,  制御装置 ,  探索問題
準シソーラス用語： *SPIN ,  モジュラ方式 ,  結合度 ,  *状態爆発問題 ,  振舞い ,  列車運行制御システム

分類 (1件)： 計算機システム開発  (JD02010R)

引用文献 (5件)：

• Mordechai Ben-Ari 著,中島震 監訳:SPINモデル検査入門,オーム社,2010.
• 小山恭平ら:情報制御システムのモデル検査における状態空間分割による探索手法の提案,ソフトウェア工学の基礎 XIX,近代科学社,Vol.38,pp.39-44,2012.
• Carlo Alberto Furia:A Compositional World - a survey of recent works on compositionality in formal methods, Technical Report 2005.22, Dipartimento di Elettronica e Informazione, Politecnico di Milano, 2005.
• Cormac Flanagan, Shaz Qadeer:Thread-Modular Model Checking, Model Checking Software Lecture Notes in Computer Science, Volume 2648, pp.213-224, 2013.
• Kedar S.Namjoshi:Model Checking in Bits and Pieces, Electronic Proceedings in Theoretical Computer Science (EPTCS) 129, pp. 404-416, 2013.

タイトルに関連する用語 (4件)： 手法 ,  モデル検査 ,  検証 ,  実用化