| Project/Area Number |
23220002
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (S)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
FUTATSUGI Kokichi 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 特任教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OGATA KAZUHIRO 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (30272991)
AOKI TOSHIAKI 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
NAKAMURA MASAKI 富山県立大学, 工学部, 講師 (40345658)
|
|---|
| Co-Investigator(Renkei-kenkyūsha) |
CHIBA YUKI 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (10509756)
SEINO TAKAHIRO 産業技術総合研究所, 社会知能研究ラボ, 特別研究員 (10397226)
|
|---|
| Research Collaborator |
PREINING Norbert 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 准教授 (60571247)
GAINA Daniel 北陸先端科学技術大学院大学, ソフトウェア検証研究センター, 助教 (80595778)
|
|---|
| Project Period (FY) |
2011-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥174,590,000 (Direct Cost: ¥134,300,000、Indirect Cost: ¥40,290,000)
Fiscal Year 2015: ¥35,880,000 (Direct Cost: ¥27,600,000、Indirect Cost: ¥8,280,000)
Fiscal Year 2014: ¥37,050,000 (Direct Cost: ¥28,500,000、Indirect Cost: ¥8,550,000)
Fiscal Year 2013: ¥37,570,000 (Direct Cost: ¥28,900,000、Indirect Cost: ¥8,670,000)
Fiscal Year 2012: ¥37,050,000 (Direct Cost: ¥28,500,000、Indirect Cost: ¥8,550,000)
Fiscal Year 2011: ¥27,040,000 (Direct Cost: ¥20,800,000、Indirect Cost: ¥6,240,000)
|
|---|
| Keywords | 仕様記述・仕様検証 / 形式手法 / ソフトウェア工学 / 代数仕様 / 証明スコア / CafeOBJ / 定理証明 |
|---|
| Outline of Final Research Achievements |
Methods for (1)achieving an appropriate level of abstraction and (2)combining inference and search in verification are researched as most important issues of specification verification. Cases of (3)self-updating software and (4)international standard for automotive software are developed as most important cases of specification verification.
Quite a few versions of language system for specification verification has been researched and developed by incorporating the research achievements of (1)-(4) into the CafeOBJ specification language system. The targeted innovative specification verification system is realized as the latest version of CafeOBJ specification language system that supports newly developed verification methodology and includes newly developed verification cases.
The latest version of CafeOBJ specification language system is available as freeware from the CafeOBJ web page (cafeobj.org) and can be executed on UNIX/Linux, MacOS, and Windows.
|
| Assessment Rating |
Verification Result (Rating)
A
|
Assessment Rating |
Result (Rating)
A: Progress in the research is steadily towards the initial goal. Expected research results are expected.
|
