2015 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) |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (30272991)
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
中村 正樹 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| Project Period (FY) |
2011-04-01 – 2016-03-31
|
| Keywords | 仕様記述・仕様検証 / 形式手法 / 代数仕様 / 証明スコア / 定理証明 / CafeOBJ |
|---|
| Outline of Annual Research Achievements |
仕様検証法研究と事例開発を相互補完的に展開しつつ、それらの成果をCafeOBJ仕様言語システムに組み込むことで、革新的仕様検証システムを構築した。
適切な抽象度の実現については，CafeOBJ言語の順序ソート機能を使い観測遷移システム(OTS)の観測子の引数の詳細化を系統的に行う技術と、状態を観測子の集合または列とすることで観測子を必要な詳細度で参照・捨象する技術を整理体系化した。
推論型×探索型検証法については，(i)Generate&Check法を支援する汎用ライブラリをCafeOBJのパラメータ化モジュールとして整理体系化し論文発表するとともに，(ii)構成子に基づく帰納的検証システム(CITP)をCafeOBJ言語システムに組み込み推論型証明支援を実現した。
ソフトウェア自動更新事例については，ソフトウェア自動更新のOTS(観測遷移システム) による形式化とそれに基づく形式検証技術を完成し論文発表した。車載OS標準事例については，車載OS国際標準OSEK/VDX Operating System 2.2.3 （英文86ページの国際標準）のCafeOBJ形式仕様と、それに基づくデッドロックや優先度逆転が発生しないことの形式検証を完成し、その成果をウェッブページを通じて発信した。
上記の成果をCafeOBJ形式仕様言語システムへ統合することで、革新的仕様検証システムを完成し、ホームページ(cafeobj.org)を通じて世界に向けて発信した。
|
| Research Progress Status |
27年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
27年度が最終年度であるため、記入しない。
|
Research Products
(15 results)
-
-
-
[Journal Article] CafeInMaude: A CafeOBJ Interpreter in Maude2016
Author(s)
Adrian Riesco, Kazuhiro Ogata, Kokichi Futatsugi
-
Journal Title
Springer Lecture Notes in Computer Science (Fundamental Approaches to Software Engineering, 19th FASE)
Volume: 9633
Pages: 377-380
DOI
Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
-
-
-
-
-
