| 研究課題/領域番号 |
23220002
|
|---|
| 研究種目 |
基盤研究(S)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
二木 厚吉 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 特任教授 (50251971)
|
|---|
| 研究分担者 |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (30272991)
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
中村 正樹 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| 連携研究者 |
千葉 勇輝 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (10509756)
清野 貴博 産業技術総合研究所, 社会知能研究ラボ, 特別研究員 (10397226)
|
|---|
| 研究協力者 |
PREINING Norbert 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 准教授 (60571247)
GAINA Daniel 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 助教 (80595778)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2016-03-31
|
| キーワード | 仕様記述・仕様検証 / 形式手法 / ソフトウェア工学 / 代数仕様 / 証明スコア / CafeOBJ / 定理証明 |
|---|
| 研究成果の概要 |
仕様検証法の最重要課題として(1)適切な抽象度と(2)推論型×探索型検証を実現する技術の研究を、重要な仕様検証事例として(3)ソフトウェア自動更新と(4)車載OS標準の事例開発を、補完的に推進した。(1)-(4)の成果を、CafeOBJ仕様言語システムに統合することで、革新的仕様検証システムを実現した。本研究の成果である[革新的仕様検証システム=最新版CafeOBJ仕様言語システム]はホームページ(cafeobj.org)を通じてフリーウェアとして入手可能であり、UNIX/Linux, MacOS, Windowsの３つの主要なプラットホームで実行可能である。
|
| 自由記述の分野 |
形式手法，仕様検証、ソフトウェア工学
|
