振る舞い仕様の効率的な実現可能性判定のための分割検証法

時間論理などでシステムの振る舞いに関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，特に計算コストが高いリアクティブシステム仕様の実現可能性判定の効率化を目的として，分割検証法について検討する．ここで検討する分割検証の枠組みは次のとおりである：(1)仕様をいくつかのサブモジュールに分割，(2)各サブモジュール仕様について，それと等価なωオートマトンを構成，(3)各サブモジュール仕様のオートマトンに簡約などを適用，(4)各サブモジュール仕様のオートマトンを統合，(5)統合したオートマトンを分析．このような分割検証では，ステップ3の簡約方法が全体としての効率を大きく左右する．本研究では，そこへ新たなアイディアを導入する．既存研究では，単なるオートマトンの最小化（等価な変換）しか行われていなかったが，本研究では，統合後の検証で不必要な局所的な情報の除去（意味的にも異なる変換）も行う．2022年度は，サブモジュール仕様のオートマトンの簡約において，局所的な「応答イベント」の情報を除去する分割検証を提案した（リアクティブシステム仕様は要求イベントと応答イベントの生起タイミングを規定するものである）．そして，その正当性，つまり，提案した方法では局所的な応答イベント情報の除去を行っても正しく実現可能性の判定が行えること（除去しないときと同様の判定結果が得られること）を証明した．

時間論理などでシステムの振る舞いに関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，特に計算コストが高いリアクティブシステム仕様の実現可能性判定の効率化を目的として，分割検証法について検討する．ここで検討する分割検証の枠組みは次のとおりである：(1)仕様をいくつかのサブモジュールに分割，(2)各サブモジュール仕様について，それと等価なωオートマトンを構成，(3)各サブモジュール仕様のオートマトンに簡約などを適用，(4)各サブモジュール仕様のオートマトンを統合，(5)統合したオートマトンを分析．このような分割検証では，ステップ3の簡約方法が全体としての効率を大きく左右する．本研究では，そこへ新たなアイディアを導入する．既存研究では，単なるオートマトンの最小化（等価な変換）しか行われていなかったが，本研究では，統合後の検証で不必要な局所的な情報の除去（意味的にも異なる変換）も行う．2022年度は，サブモジュール仕様のオートマトンの簡約において，局所的な「応答イベント」の情報を除去する分割検証を提案した（リアクティブシステム仕様は要求イベントと応答イベントの生起タイミングを規定するものである）．そして，その正当性，つまり，提案した方法では局所的な応答イベント情報の除去を行っても正しく実現可能性の判定が行えること（除去しないときと同様の判定結果が得られること）を証明した．