2014 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-04-01 – 2016-03-31
|
| Keywords | 仕様記述・仕様検証 / 形式手法 / 代数仕様 / 証明スコア / CafeOBJ |
|---|
| Outline of Annual Research Achievements |
仕様記述検証法と事例開発を相互補完的に継続しつつ、それらの成果をCafeOBJ仕様言語システムに組み込むことで革新的仕様検証システムの構築を推進した。
適切な抽象度の実現法については、OTS(Observational Transition System,観測遷移システム)の状態を、観測子の列(sequence)で表現し、必要な詳細度で参照・捨象する技術を確立した。推論型×探索型検証法については、構成子論理(constructor-based logic)に基づく証明支援システム(CITP)と証明スコアを融合する手法を開発した。これらにより、適切な抽象度で仕様記述検証を行う技術を大きく推進した。
ソフトウェア自動更新事例については、ソフトウェア自動更新のOTSによる形式化に基づき、推論型検証と探索型検証を併用しつつ、次世代ソフトウェア自動更新の形式仕様とその検証をほぼ完成した。車載OS標準事例については、開発した国際標準の形式仕様記述スキーマと仕様検証法をベースに、ネットを通じて世界に発信できるような国際標準(OSEK/VDX Operating System 2.2.3) のCafeOBJ形式仕様をほぼ完成し、デッドロックや優先度逆転の形式検証の中核部分も完成した。
革新的仕様検証システムの構築については、上記の成果を適宜CafeOBJ仕様言語システムに組み込みつつ、言語システムと連携したオンライン文書化機能と、状態探索コマンドの遷移システム検証の基本ツールとしての機能を強化した。また、仕様の停止性、合流性、十分完全性のモジュラーな判定アルゴリズムの設計を推進し、構成子論理に基づく定理証明支援サブシステムのプロトタイプを完成した。こららにより、最終年度である2015年度に、計画通り革新的仕様検証システムを構築できる見通しを得た。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
革新的仕様検証システムの構築を目標に、(1)仕様検証の中核技術である適切な抽象度と推論型×探索型検証法を実現する技術、(2)実用的に重要な事例であるソフトウェア自動更新事例と車載OS標準事例、の研究開発を進めてきた。それぞれの項目について、以下の通り全体として予定通りに、あるものについては予想以上に進展している。
仕様記述検証技術については、適切な抽象度を観測子の列表現に基づき系統的に実現する技術は、類例がなく新規性・独自性が高い。またこの技術に基づき適切な抽象度で推論型×探索型検証法を実現する技術が開発できた。これは仕様記述検証技術に関する当初の予想を上回る成果である。
ソフトウェア自動更新事例については、既に実用化が始まっている次世代ソフトウェア自動更新に対し、仕様記述検証の基盤を確実なものにできた。車載OS標準事例については、現実の国際標準であるOSEK/VDXの形式仕様に基づき、実装方法などの詳細に立ち入らず適切な抽象度でデッドロックや優先度逆転の形式検証を行う方法の体系化を進展させた。このように２つの事例開発は順調に進展している。
革新的仕様検証システムの構築は、最終年度（2015年度）に革新的仕様検証システムを完成すべく、仕様記述検証と事例開発の成果をCafeOBJ仕様言語システムに組み込みつつ、順調に進展している。とくに、構成子論理に基づく証明支援(CITP)のプロトタイプをCafeOBJ仕様言語システムのサブシステムとして実現できたことは、予想以上の成果である。
|
| Strategy for Future Research Activity |
最終年度である2015年度は、CafeOBJ仕様言語システム(cafeobj.org)に仕様検証技術と事例開発の研究成果を組み込むことで、革新的仕様検証システムを完成すべく、研究開発を以下のように展開する。
適切な抽象度の実現については、状態遷移システムに焦点を絞り、観測子の列として表現される状態パターンに基づく詳細化/抽象化手法を開発する。推論型×探索型検証法については、すでにCafeOBJのサブシステムとして開発済みの構成子論理に基づく証明支援機能(CITP)と証明スコアの融合した仕様検証技術を開発する。
次世代ソフトウェア自動更新については、その形式記述検証の枠組みを完成させ、車載OS標準事例については、国際標準OSEK/VDX Operating System 2.2.3（英文86ページ）形式仕様と形式検証のホームページを完成する。
上記の仕様検証技術と事例開発の成果をCafeOBJ仕様言語システムに組み込むことで革新的仕様検証システムを完成し、CafeOBJホームページ(cafeobj.org)を通じて世界に発信する。
|
