有界モデル検査を用いた複数UML図の形式的検証

概要

論文の詳細を見る
筆者らはこれまでに,システム開発における複数のUML図で記述された仕様を一つの状態機械としてモデル化し,モデル検査による検証を行う手法について検討を行ってきた.また,検証の対象となるシステムが大規模である場合に状態数が爆発的に増加する,いわゆる状態爆発問題に対し,有界モデル検査(Bounded Model Checking, BMC)を用いて状態爆発を避ける手法についても検討してきた.有界モデル検査はシステムの探索する状態をある有限のステップ数に限定することで,大規模なシステムの検証を可能とする.しかしながら,有界モデル検査を用いたとしても状態爆発が避けられない問題も存在する.そこで本論分では,状態の探索手法であるForward SearchとBackward Searchの二つを用いた検証をそれぞれ比較し,より有効な探索手法についての検討を行うことで,有界モデル検査の効率化を目指す.比較実験として,UMLの状態遷移図とシーケンス図を用いて記述されたソフトウェアの仕様を対象として,Forward SearchとBackward Searchのそれぞれを用いて有界モデル検査を行った.また,従来の非有界モデル検査(Unbounded Model Checking, UBMC)による検証との比較についても示した.
社団法人電子情報通信学会の論文
2008-02-25