反例からの検査式自動生成による不具合原因特定支援

摘要

モデル検査はシステムの振る舞いを検証するためには有効な技術である．我々はモデル検査技術を利用して仕様書とソースコードの振る舞いの不一致を発見する手法を提案してきた．この手法により不一致の有無は明示されるが，その不一致が起こる原因を特定するためには反例を解析する必要があった．出力される反例は状態遷移のトレースであり，その意味を理解するには複雑な状態遷移を追跡して意味を読み取らなければならないため、一般的な開発者にとっては解析が難しい．本稿では，出力された反例にあるシステムの振舞いの状態を抽出して，検査式に付加することにより状態遷移の特定を試みる．反例が出たら，再度システムの振舞いの状態を抽出して検査式に付加して検査するサイクルを繰り返すことにより、問題となる状態遷移の特定を容易にする手法を提案する．