5A-3
モデル検査自動化ツールの開発～入力支援機能と状態遷移表縮約機能～
○森奈実子，高田沙都子，長谷川保，村田由香里，進 博正（東芝）
モデル検査はシステムの仕様を有限の状態遷移空間として表現し，
状態遷移系を網羅的に探索することで，上流工程において不具合の
有無を検証することができる．また，筆者らが開発しているモデル
検査自動化ツールでは，状態遷移表からの検査用モデル生成などに
より導入障壁を低くするよう努めている．しかし，製品開発への適
用において，状態遷移表が存在しない，あるいは大規模かつ複雑な
システムのため状態爆発が懸念されるなど問題が浮上している．
そこで本稿では，状態遷移図やフローチャートから状態遷移表を
生成する入力支援機能や状態遷移表縮約機能について紹介する．