| 研究課題/領域番号 |
23220002
|
|---|
| 研究種目 |
基盤研究(S)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
二木 厚吉 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 特任教授 (50251971)
|
|---|
| 研究分担者 |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (30272991)
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
中村 正樹 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| 連携研究者 |
千葉 勇輝 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (10509756)
清野 貴博 産業技術総合研究所, 社会知能研究ラボ, 特別研究員 (10397226)
|
|---|
| 研究協力者 |
PREINING Norbert 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 准教授 (60571247)
GAINA Daniel 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 助教 (80595778)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
174,590千円 (直接経費: 134,300千円、間接経費: 40,290千円)
2015年度: 35,880千円 (直接経費: 27,600千円、間接経費: 8,280千円)
2014年度: 37,050千円 (直接経費: 28,500千円、間接経費: 8,550千円)
2013年度: 37,570千円 (直接経費: 28,900千円、間接経費: 8,670千円)
2012年度: 37,050千円 (直接経費: 28,500千円、間接経費: 8,550千円)
2011年度: 27,040千円 (直接経費: 20,800千円、間接経費: 6,240千円)
|
|---|
| キーワード | 仕様記述・仕様検証 / 形式手法 / ソフトウェア工学 / 代数仕様 / 証明スコア / CafeOBJ / 定理証明 |
|---|
| 研究成果の概要 |
仕様検証法の最重要課題として(1)適切な抽象度と(2)推論型×探索型検証を実現する技術の研究を、重要な仕様検証事例として(3)ソフトウェア自動更新と(4)車載OS標準の事例開発を、補完的に推進した。(1)-(4)の成果を、CafeOBJ仕様言語システムに統合することで、革新的仕様検証システムを実現した。本研究の成果である[革新的仕様検証システム=最新版CafeOBJ仕様言語システム]はホームページ(cafeobj.org)を通じてフリーウェアとして入手可能であり、UNIX/Linux, MacOS, Windowsの３つの主要なプラットホームで実行可能である。
|
| 評価記号 |
検証結果 (区分)
A
|
評価記号 |
評価結果 (区分)
A: 当初目標に向けて順調に研究が進展しており、期待どおりの成果が見込まれる
|
