研究課題
基盤研究(C)
ソフトウェア自動検証の技術として注目を集めているモデル検査法は有限の状態空間を網羅的に探索して時相論理式で表現した性質を満たすか否かを判定する。データ値が制御の流れに影響する場合、データ値の範囲が大きい等の理由により状態爆発の問題が発生する。本研究では状態爆発を避けるために、「制約記述を用いた値評価の遅延方法」をモデル検査法と統合するための技術を検討した。変数が取りえるデータ値を具体的に扱うのではなく、データ値に関する性質を記号的な制約として表現することで状態爆発を避ける方法である。さらに、データの性質表現を簡明に行うために代数仕様の方法を導入し、代数仕様言語Maudeを用いてデータ制約とモデル検査法を統合する技術に関する研究を進めた。具体的には、1.ソフトウェアデザインで用いられるMealy型オートマトンに制約概念を導入した「制約オートマトン」の定式化とMaude上での実現方法の考案、2.区間制約、分散ソーティング、ホテル鍵問題、の3つの例題を用いての提案方式の確認、特に、ホテル鍵問題については公表されているAlloyによる記述と解析の方法との比較により提案方法の有用性を確認、3.RT-Maudeを用いて制約オートマトンを実現することでリアルタイム・ソフトウェアへの応用検討、を行った。また、今後の研究の展開に関する計画として、定理証明を基礎とするEvent-Bの振舞い解析への応用について整理した。さらに、アウトリーチの試みとして、形式手法技術を概観するサーベイを公表した。
すべて 2008 2007 2006
すべて 雑誌論文 (6件) (うち査読あり 2件) 学会発表 (4件)
Proceedings of the IASTED International Conference on Software Engineering
ページ: 98-105
Proceedings of the TASTED International Conference on Software Engineering
情報処理学会論文誌 48
ページ: 3341-3351
Journal of Information Processing Society of Japan Vol.48, No.10
コンピュータソフトウェア 23
ページ: 72-86
Computer Software Vol.19, No.2
