2013 Fiscal Year Annual Research Report
| Project/Area Number |
23220002
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 特任教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
中村 正樹 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| Project Period (FY) |
2011-05-31 – 2016-03-31
|
| Keywords | 仕様記述・仕様検証 / 形式手法 / 代数仕様 / ソフトウェア工学 / 証明スコア / CafeOBJ |
|---|
| Research Abstract |
証明スコア法による仕様検証の中核技術として、適切な抽象度と推論型×探索型検証法を実現する技術の研究を進めるとともに、実用的に重要な事例として、ソフトウェア自動更新事例と車載OS標準事例の研究開発を進めた。さらに、それらの成果をCafeOBJ形式仕様言語システムに統合することで、革新的仕様検証システムの構築を推進した。
適切な抽象度の実現: CafeOBJ 言語の順序ソート(order sort)機能とモジュール化機能を使い観測遷移システム(OTS: Observational Transition Systems)の観測子(observer) の引数の詳細化を系統的に行う技術と、OTSの状態を観測子の集合(set)または列(sequence)で表わすことで観測子を必要な詳細度で参照する技術を研究開発した。
推論型×探索型検証法： OTSの状態を観測子の集合または列として表現し、状態遷移をその状態表現（状態パタン）上の遷移規則(trans規則)として表すことで、OTSの全ての可能な状態（一般には無限）をもれなくカバーする有限の状態パタンを系統的に生成する手法を研究開発した。さらに、この手法を用いることで不変性(invariant)が検証できることを示した。
ソフトウェア自動更新事例： 稼働中のソフトウェアを停止することなく更新できる、次世代のソフトウェア更新技術の形式モデルならびに形式検証の技術基盤を開発した。
車載OS標準事例： 適切な抽象度を実現する技術を用いて、車載OS標準のCafeOBJ形式仕様の整構造化を一層推進し、その仕様に基づきデッドロックや優先度逆転の解析・検証技術を整理体系化した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
革新的仕様検証システムの構築を目標に、仕様検証の中核技術である適切な抽象度と推論型×探索型検証法を実現する技術、実用的に重要な事例として、ソフトウェア自動更新事例と車載OS標準事例の研究開発を進めてきた。各々のテーマは、以下のような達成度である。とくに、適切な抽象度の実現、推論型×探索型検証法、車載OS標準事例では予想以上の成果を得ている。これらの成果を、言語機能、ツール、ライブラリ（事例）としてCafeOBJ形式仕様言語システムへ統合することで、革新的仕様検証システムの構築も順調に進んでおり、全体として予定通りの成果が見込まれる。
適切な抽象度の実現： 適切な抽象度を客観的に実現する技術は、類例がなく、新規性・独自性の高い成果である。とくに、この技術の有効性が車載OS 標準事例を通じて実証的に示されたのは予想以上の成果である。
推論型×探索型検証法： 時間軸だけでなく空間軸にたいする探索型検証を推論型検証とシームレスに融合した本検証技術は、全く新規のものであり、当初の目標を超える研究の進展があり、予定以上の成果があった。
ソフトウェア自動更新事例： 安全性と信頼性が極めて重要であるにもかかわらず、その検証が不十分のまま、既に実用化が始まっている次世代ソフトウェア自動更新に対し、予定通り形式検証の基盤が開発できた。
車載OS標準事例： OSEK/VDXの形式仕様に基づきデッドロックや優先度逆転が発生しないことを、実装方法などの詳細に立ち入らず、適切な抽象度で検証できたことは、予想以上の成果である。また、適切な抽象度を体系的な技術を用いて実現できた点は、当初の予想を超える進展である。
|
| Strategy for Future Research Activity |
適切な抽象度の実現については、 観測子の集合または列として定義される状態パタンの詳細化と観測子の引数の詳細化の対応関係を明確にし、その有効性を例題や事例で確認し、汎用性のある技術の確立を目指す。
推論型×探索型検証法については、 ほぼ開発を終了している「証明スコア法に基づく定理証明系(CITP)」の研究をより進展させ、それから得られる知見をベースに推論型×探索型検証法をより深化させることを目指す。
ソフトウェア自動更新事例については、推論型×探索型検証法により、次世代ソフトウェア自動更新の形式検証を完成することを目指す。
車載OS標準事例については、国際標準の形式仕様記述スキーマと仕様検証法をベースとして、ネットを通じて世界に発信できるようなOSEK/VDX Operating System 2.2.3 （英文86ページの国際標準）のCafeOBJ形式仕様の完成を目指す。
上記の研究成果を、CafeOBJ形式仕様言語システムへ適切に組込みつつ、革新的仕様検証システムの構築の完成を目指す。
|
