| 研究課題/領域番号 |
23220002
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
二木 厚吉 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 特任教授 (50251971)
|
|---|
| 研究分担者 |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (30272991)
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
中村 正樹 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2016-03-31
|
| キーワード | 仕様記述・仕様検証 / 形式手法 / 代数仕様 / 証明スコア / 定理証明 / CafeOBJ |
|---|
| 研究実績の概要 |
仕様検証法研究と事例開発を相互補完的に展開しつつ、それらの成果を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)を通じて世界に向けて発信した。
|
| 現在までの達成度 (段落) |
27年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
27年度が最終年度であるため、記入しない。
|
