• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2015 Fiscal Year Final Research Report

Development of the Innovative Specification Verification System based on Proof Scores

Research Project

  • PDF
Project/Area Number 23220002
Research Category

Grant-in-Aid for Scientific Research (S)

Allocation TypeSingle-year Grants
Research Field Software
Research InstitutionJapan 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
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.

Free Research Field

形式手法,仕様検証、ソフトウェア工学

URL: 

Published: 2017-05-10  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi