2005 Fiscal Year Annual Research Report
| Project/Area Number |
17500028
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
中島 震 国立情報学研究所, ソフトウェア研究系, 教授 (60350211)
|
|---|
| Keywords | ソフトウェア工学 / ソフトウェア開発効率 / モデル化 / 検証技術 |
|---|
| Research Abstract |
ソフトウェア自動検証の技術として、モデル検査法が注目を集めている。検証対象の振舞い仕様が構築する有限の状態空間を網羅的に探索することによって、時相論理式で表現した性質を満たすか否かを判定する。この時、取り扱うデータ値の範囲が大きい等の理由によって起こる状態爆発の問題に対応することが課題になっている。本研究では、明示的にデータ値を扱うのではなく、データ値に対する制約記述を管理し、必要になった時点で制約を解くことで値を決定する「制約記述を用いた値評価の遅延方法」を組み込むことを検討した。特に、表現力の高い代数仕様アプローチを用いることで、従来の方法では取り扱いの難しかった複雑な構造に対する制約記述を統合することを目標とした。
初年度は代数仕様言語Maudeの時相論理(LTL)モデル検査ライブラリの調査を行い、同ライブラリを用いて基本的なLTLモデル検査の予備実験を行った。また、制約概念を導入した拡張有限オートマトン(制約オートマトン)を定義し、Maudeで表現する方法を考案した。制約オートマトンは、新たな制約記述追加を可能とし、状態遷移の進行にそって、制約充足性判定を行う。充足不能であることが判明すればデッドロックとして停止する。充足可能であって値の解が求まれば正しい結果を得る。状態遷移が実現する振舞い仕様とデータ制約を統合した考え方にたつ。なお、制約オートマトンは一般的なモデルであり具体的な制約系を前提としない。次年度以降は、具体的な決定可能な制約系をMaude上で実現し、特定の応用問題に適用することで、提案方式の有効性を示す計画である。
|
Research Products
(2 results)
