| 研究課題/領域番号 |
23220002
|
|---|
| 研究種目 |
基盤研究(S)
|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| 研究分担者 |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
中村 正樹 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| キーワード | 仕様記述・仕様検証 / 形式手法 / 代数仕様 / ソフトウェア工学 / 証明スコア / CafeOBJ |
|---|
| 研究概要 |
問題仕様にたいする適切な抽象度と推論型×探索型検証法の実現を目標とし、電子商取引プロトコルと車載OS標準の2つの事例の開発を進めつつ、申請時に作成した計画の妥当性を検証した。具体的には以下の研究成果を得た。
1.適切な抽象度の実現:CafeOBJの形式仕様作成について、問題を記述するのに必要なデータとプロセスを適切に切り分け、データ型とプロセス型として定義することが、適切な抽象度の実現に重要であるとの知見を得ていた。2つの事例開発を進めることで、この知見の有効性を確認した。
2.推論型×探索型検証法の実現:推論×探索型検証法のシームレスな実現の基盤として、推論型検証向きのシステム仕様を探索型検証向きのシステム仕様に変換する方法を開発し実装した。推論型検証向きのシステム仕様として、等式を用いてシステムの振舞いを記述したシステム仕様を採用し、探索型検証向きのシステム仕様とは、書換え規則を用いてシステムの振舞いを記述したシステム仕様を採用した。変換器をMaudeシステムのメタ機能を用いて実装し、電子商取引プロトコルを含むいくつかの例題による実験により、本方法の有効性を確認した。
3.電子商取引プロトコル事例:iKPプロトコルに対し、推論型×探索型検証法により反例発見と検証を相互補完的に適用しながら、CafeOBJ形式仕様と証明スコアを開発した。これにより、本プロジェクトの目標達成のためには,電子商取引アプリケーションに限定せず、より一般的な展望のものに,クラウドコンピューティングなどの進展により重要性が高まりつつある、ミドルウェアプロトコルを対象とするのが適当であるとの知見を得た。
4.車載OS標準事例:AUTOSARが公開しているOSEK/VDX仕様のプロセス管理部分に対し、CafeOBJ形式仕様のプロトタイプを完成した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
問題仕様にたいする適切な抽象度と推論型×探索型検証法の実現に関する、仕様記述・仕様検証法に関する研究は計画通りに進展している。2つの事例開発のうち、車載OS標準に関してはCafeOBJ形式仕様をプロトタイプが完成し予想以上に進展した。電子商取引プロトコルについては,事例開発は順調に進展したが、当該分野の最近の展開と将来展望に基づき、より一般的なミドルウェアプロトコルを対象とするのが適当であると判断した。全体として、おおむね順調に進展している。
|
| 今後の研究の推進方策 |
初年度であるH23年度は、計画通りに研究を遂行すると同時に、申請時の計画の妥当性と実効性を検証することも目標とした。その結果、プロトコルの検証事例開発については、当該分野の最近の展開と将来展望に基づき、より一般的なミドルウェアプロトコルを対象とするのが適当であると判断し、研究計画をそのように変更することとした。また、H24年度からは、並行して展開している複数の研究活動を、最終目標であるCafeOBJ言語システムの革新に向けた設計実装に収斂させる活動を開始する予定である。
|
