|
形式仕様検証は人力では見つけにくい欠陥を検出できるが，その計算コストは高い．本研究では，リアクティブシステム仕様の非制限的検証，つまり仕様の構文や検証性質を制限しない検証のコスト削減を目的として，以下に取り組んだ．(1)リアクティブシステム仕様の検証で基盤となるωオートマトンや無限ゲームの効率的な操作手法を提案した．具体的には，無限ゲームの簡約方法や，部分シンボリック技法を用いたωオートマトンや無限ゲームの各種操作の効率的な実装手法を提案した．(2) 提案したωオートマトンや無限ゲームの効率的な操作手法を基に仕様検証器を開発した．
|
