| 研究課題/領域番号 |
18500019
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
|
|---|
| 研究期間 (年度) |
2006 – 2008
|
| 研究課題ステータス |
完了 (2008年度)
|
| 配分額 *注記 |
4,350千円 (直接経費: 3,600千円、間接経費: 750千円)
2008年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2007年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2006年度: 1,100千円 (直接経費: 1,100千円)
|
|---|
| キーワード | 仕様記述 / 仕様検証 / モデル検査 / 仕様変換 / 観測遷移システム / CafeOBJ、Maude / メタプログラミング / 定理証明 / 変換 / CafeOBJ / Maude / 変換器 / 有界モデル検査 / 数学的帰納法 / 反例 / 補題 / IGF / 補題発見 |
|---|
| 研究概要 |
証明支援系とモデル検査器を効果的に利用できるよう、定理証明向きのシステム仕様をモデル検査向きのシステム仕様に自動変換する方法を考案した。変換により、モデル検査向きのシステム仕様が大きくなりすぎて効果的にモデル検査ができなくなることを防ぐための工夫を行った。提案した変換方法の有効性を確認するため、電子商取引プロトコルiKPとMondex の検証実験に適用した。また、変換を支援する変換ツールの拡張性の高い実装方法も提案した。この実装方法では、複数の変換規則をモジュラーに組み入れることを可能にする。
|
