| 研究課題/領域番号 |
17500028
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
中島 震 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60350211)
|
|---|
| 研究期間 (年度) |
2005 – 2007
|
| 研究課題ステータス |
完了 (2007年度)
|
| 配分額 *注記 |
3,700千円 (直接経費: 3,400千円、間接経費: 300千円)
2007年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2006年度: 1,400千円 (直接経費: 1,400千円)
2005年度: 1,000千円 (直接経費: 1,000千円)
|
|---|
| キーワード | ソフトウェア工学 / ソフトウェア開発効率化 / モデル化 / 検証技術 / モデル検査 / 代数仕様 / データ制約 / ソフトウェア開発効率 |
|---|
| 研究概要 |
ソフトウェア自動検証の技術として注目を集めているモデル検査法は有限の状態空間を網羅的に探索して時相論理式で表現した性質を満たすか否かを判定する。データ値が制御の流れに影響する場合、データ値の範囲が大きい等の理由により状態爆発の問題が発生する。本研究では状態爆発を避けるために、「制約記述を用いた値評価の遅延方法」をモデル検査法と統合するための技術を検討した。変数が取りえるデータ値を具体的に扱うのではなく、データ値に関する性質を記号的な制約として表現することで状態爆発を避ける方法である。さらに、データの性質表現を簡明に行うために代数仕様の方法を導入し、代数仕様言語Maudeを用いてデータ制約とモデル検査法を統合する技術に関する研究を進めた。具体的には、1.ソフトウェアデザインで用いられるMealy型オートマトンに制約概念を導入した「制約オートマトン」の定式化とMaude上での実現方法の考案、2.区間制約、分散ソーティング、ホテル鍵問題、の3つの例題を用いての提案方式の確認、特に、ホテル鍵問題については公表されているAlloyによる記述と解析の方法との比較により提案方法の有用性を確認、3.RT-Maudeを用いて制約オートマトンを実現することでリアルタイム・ソフトウェアへの応用検討、を行った。また、今後の研究の展開に関する計画として、定理証明を基礎とするEvent-Bの振舞い解析への応用について整理した。さらに、アウトリーチの試みとして、形式手法技術を概観するサーベイを公表した。
|
