複雑なシステムの仕様を簡潔に記述する手法にStatechartを用いる
方法がある．本研究ではStatechartで記述された仕様が，望ましい
性質を満たしているかどうかを自動検証することを試みる．ここで
検証ツールとしてSMV(Symbolic Model Verifier)を利用する．SMV
はモデル化したシステムの状態空間や遷移関係を２分決定グラフ
(OBDD)で表現することで状態爆発の問題を避ける事ができ，主に
ハードウェアシステムの検証で広く利用されている．具体的には
StatechartをSMVの入力言語(SMV language)に変換する方法を開発
することで自動検証を実現する．
Back