|
自動検証の方法として注目されているモデル検査法では「状態爆発の問題」への対応が不可欠である。本研究課題では、変数が多くの値をとりえる場合の状態爆発問題を解決するためにデータ制約の方法を提案した。個別の値に対する網羅的な検査を行う替わりに、変数値に対する条件を代数的な方法で表現した記号制約を対象としてモデル検査を行う。複数の値を取りえる可能性がある場合であっても記号表現した制約ひとつだけを検査すればよい。具体的な方法としてMaudeを用いた。平成19年度は前年度までの成果を論文としてまとめて公表した。また、ソフトウェアのデザイン検証への応用に関する研究を進め、特に、リアルタイム性を持つ分散ソフトウェアのタイミング解析への適用法を検討した。従来のモデル検査法ではシステム全体にわたって抽象化を行うことで状態爆発の問題を回避していた。ところが、外部とのインタラクションが重要なリアルタイムソフトウェアでは、外部入力データを抽象化すると情報がなくなるという問題がある。外部とのインタフェースだけは抽象化しない方法が望ましい。本研究では、外部インタフェースにデータ制約の方法を導入することで、入力データ値に依存した振舞い解析を精度よく行う方法を実験した。Real-Time Maude上で行った簡単な事例を用いた実験結果を国際会議で発表した。さらに、同様なインタフェース抽象化への応用が重要となるようなソフトウェアのデザイン記述法についての調査研究も並行して行い、Event-B要求仕様記述の解析が課題になっていることがわかった。
|
