5A-2
モデル検査自動化ツールの開発～検査自動化と反例解析効率化～
○高田沙都子，森奈実子，村田由香里（東芝）
モデル検査はシステムの仕様を有限の状態遷移空間として表現し，
状態遷移系を網羅的に探索することで，上流工程において不具合の
有無を検証することができる．しかし，モデル検査を適用するため
には検査用モデルや検査式の作成などの導入コストを低くする必要
がある．そこで，状態遷移表を仕様として入力すると検査用モデル
の生成から検査の実行までを自動的に行うツールを開発した．この
ツールは，反例をチャート化し可読性を向上させ，状態遷移表上で
追跡しながら原因を分析する補助機能も備えている．本稿では，本
開発ツールの機能と有効性について紹介する．