2006 Fiscal Year Annual Research Report
| Project/Area Number |
17500028
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
中島 震 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60350211)
|
|---|
| Keywords | ソフトウェア工学 / ソフトウェア開発効率 / モデル化 / 検証技術 |
|---|
| Research Abstract |
ソフトウェア自動検証の技術として、モデル検査法が注目を集めている。本研究では、明示的にデータ値を扱うのではなく、データ値に対する制約記述を管理し、必要になった時点で制約を解くことで値を決定する「制約記述を用いた値評価の遅延方法」を組み込むことを検討した。特に、表現力の高い代数仕様アプローチを用いることで、従来の方法では取り扱いの難しかった複雑な構造に対する制約記述を統合することを目標とした。
前年度行った代数仕様言語Maudeを用いた制約オートマトンの予備実験の成果をもとに、制約オートマトンの定義を明確化し、Maudeが提供する状態空間探索法の制約オートマトン解析への適用方法を整理した。また、具体的な例題を記述することで制約オートマトンの有用性を考察した。最初に、整数リストをソートする「分散ソート」の例題を扱い、具体的な値を与えなくても、整数に関する大小関係という制約条件を与えるだけで解析が可能なことを示した。2番目に「ホテル鍵問題」と呼ぶデータ制約と共に状態遷移の考え方の双方が必要になる例題を、制約オートマトンの考え方で記述・解析した。これはデータ制約を中心とする形式仕様記述ならびに解析ツールAlloyで取り扱っている例題である。本研究の方法との記述・解析の比較を行い、制約オートマトンの有用性を考察した。
また、他の性質を持つソフトウェアデザインに制約オートマトンの考え方を適用できるかの調査を行い、解説記事として整理して公表した。この調査の一貫として調べたEvent-Bと呼ぶ形式手法は、本質的に振る舞い仕様が重要であるにも関わらず、現在のツールは扱っていないことがわかった。Event-Bはデータ制約が重要な役割を果たす形式仕様言語であり、制約オートマトンで興味ある解析が可能と考えられる。来年度、この方向の研究を進める。
|
