| 研究課題/領域番号 |
23220002
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| 研究分担者 |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
中村 正樹 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| 研究期間 (年度) |
2011-05-31 – 2016-03-31
|
| キーワード | 仕様記述・仕様検証 / 形式手法 / 代数仕様 / ソフトウェア工学 / 証明スコア / CafeOBJ |
|---|
| 研究概要 |
証明スコア法による仕様検証の中核技術として，1. 適切な抽象度と2.推論型×探索型検証法を実現する技法の研究開発を進めるとともに，実用的に重要な事例として，3.ミドルウェアプロトコルと4.車載OS標準の事例開発を進め，以下の成果を得た。
1.適切な抽象度の実現： OTS(Observational Transition System)のスキーマを用い，データ型とプロセス型を適切に切り分けつつ，適切な抽象度を実現する方法を開発した．具体的には，OTSの状態を観測子(observer)の集合として表わすことで，検証すべき性質に応じて，必要な観測子を必要な詳細度で参照し，他の観測子を捨象することを可能とした．
2.推論型×探索型検証法の実現： 観測子の集合として表わされたOTSの全ての可能な状態（一般には無限）をもれなくカバーする記号的な有限集合を系統的に生成し，その全てについて望みの性質が成り立つことをチェックする方法を開発した．①と②の研究成果から，「適切な抽象度と推論型×探索型検証法は補完的に強力な仕様検証法の実現に寄与する」という知見を得た．
3.ミドルウェアプロトコル事例： 重要性が高まりつつあるクラウドコンピューティング事例に焦点を当て研究を進めた．研究協力関係に有る復旦大学(Fudan Univ., 中国上海)で開発された動的ソフトウェア更新プロトコルPOLUSの調査研究に基づき，動的ソフトウェア更新のモデルを提案し，定理証明（推論型）とモデル検査（探索型）を用いた検証実験を行い，提案したモデルの有効性を確認した．
4.車載OS標準事例：OSEK/VDXのプロセス管理を規定した国際標準(英文と図表かなる100ページ弱の文書)のCafeOBJ言語による形式仕様の第１版を完成し，その仕様に基づきデッドロックの発生の有無の検証・解析を行った．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
適切な抽象度と推論型×探索型検証法の実現を通じての仕様検証法の研究開発は，OTSの状態を観測子の集合としてモデル化する技法に焦点を当てることで，予想以上の進展があった．電子商取引，ミドルウェアプロトコル，クラウドコンピューティング事例については，クラウドコンピューティングの動的ソフトウェア更新事例に焦点を当て順調に進展している．車載OS標準事例は形式仕様をすでに完成し解析・検証を開始できた．全体として，当初の計画以上に進展している．
|
| 今後の研究の推進方策 |
H24年度までの２年間で適切な抽象度と推論型×探索型検証法の２つを統一的な仕様検証法に統合する見通しを得た．H25年以降は事例開発との融合を進めるとともに，言語システムへの統合を進める．電子商取引，ミドルウェアプロトコル，クラウドコンピューティング事例については，H25年度以降，クラウドコンピューティングの動的ソフトウェア更新事例に焦点を当て研究開発を進める．
H24年度は見積額と実施額の間に差が有り未使用額が生じたが，今後はこうしたことが無いようにしたい．
|
