| 研究課題/領域番号 |
23240004
|
|---|
| 研究種目 |
基盤研究(A)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| 研究分担者 |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
|
|---|
| 研究期間 (年度) |
2011
|
| 研究課題ステータス |
完了 (2011年度)
|
| 配分額 *注記 |
15,080千円 (直接経費: 11,600千円、間接経費: 3,480千円)
2011年度: 15,080千円 (直接経費: 11,600千円、間接経費: 3,480千円)
|
|---|
| キーワード | 仕様記述・仕様検証 / 形式手法 / 形式仕様 / 問題仕様 / ソフトウェア工学 / 証明スコア / CafeOBJ / 観測遷移システム |
|---|
| 研究概要 |
証明スコア法により問題仕様(問題領域や応用領域における組織、規則、活動、処理の仕様やモデル)の検証を可能とする革新的仕様検証技術の開発を目指して研究を行い、以下の成果を得た。
1適切な抽象度の実現法について、提案している観測遷移シヌテム(OTS:Observational Transition System)がデータ型とプロセス型を適切に定義することで、適切な抽象度を実現する一般的なスキーマと成り得ることを、実用規模の事例開発を通じて確認した。
2推論型×探索型検証法の実現法について、(1)帰納法に基づく反例発見法(IGF:Induction Guided Falsification)と(2)推論に基づく抽象化と探索に基づく反例発見を組み合わせる方法、の2つの方法が有効であることを例題に基づき確認した。
3電子商取引プロトコル事例については、上記の「推論型×探索型検証法」を実例に基づき確認することに焦点を当てて研究を行った。具体的にはiKP(Internet Keyed Payment Protocols)を取り上げ、帰納法に基づく反例発見法(IGF)の有効性を確認した。この事例開発では、CafeOBJ言語システムで形式仕様を開発し、Maude言語システムの高効率の探索機能を利用する方法論についても研究を行い、そのための方法論と支援ツールも開発した。
4車載OS標準事例については、AUTOSARが公開し世界的に認知度が高いOSEK/VDX仕様(portal.osek-vdx.org/files/pdf/specs/os223.pdf)に対して、CafeOBJ言語で記述された形式仕様を開発した。この仕様開発において、観測遷移システム(OTS)に基づく形式仕様開発方法論の有効性を確認した。
|
