|
JAIST Repository >
ソフトウェア検証研究センター 2010～2016 >
z9-50. 科学研究費助成事業研究成果報告書 >
2015年度 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/13692
|
| タイトル: | 証明スコア法に基づく革新的仕様検証システムの構築 |
| その他のタイトル: | Development of the Innovative Specification Verification System based on Proof Scores |
| 著者: | 二木, 厚吉 |
| 著者（別表記）: | Kokichi, Futatsugi |
| キーワード: | 仕様記述・仕様検証
形式手法
ソフトウェア工学
代数仕様
証明スコア
CafeOBJ
定理証明 |
| 発行日: | 18-May-2016 |
| 抄録: | 仕様検証法の最重要課題として(1)適切な抽象度と(2)推論型×探索型検証を実現する技術の研究を、重要な仕様検証事例として(3)ソフトウェア自動更新と(4)車載OS標準の事例開発を、補完的に推進した。(1)-(4)の成果を、CafeOBJ仕様言語システムに統合することで、革新的仕様検証システムを実現した。本研究の成果である[革新的仕様検証システム=最新版CafeOBJ仕様言語システム]はホームページ(cafeobj.org)を通じてフリーウェアとして入手可能であり、UNIX/Linux, MacOS, Windowsの３つの主要なプラットホームで実行可能である。 : 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. |
| 記述: | 基盤研究(S)
研究期間：2011～2015
課題番号：23220002
研究者番号：50251971
研究分野：形式手法、仕様検証、ソフトウェア工学 |
| 言語: | jpn |
| URI: | http://hdl.handle.net/10119/13692 |
| 出現コレクション: | 2015年度 (FY 2015)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| 23220002seika.pdf | | 569Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
