証明スコア法に基づく革新的仕様検証システムの構築

• 資料種別: 文書・図像類
• タイトル: 証明スコア法に基づく革新的仕様検証システムの構築
• 著者・編者: 二木, 厚吉
• 著者標目: 二木, 厚吉
• 出版年月日等: 2016-05-18
• 出版年（W3CDTF）: 2016-05-18
• 並列タイトル等: Development of the Innovative Specification Verification System based on Proof Scores
• タイトル（掲載誌）: 科学研究費助成事業研究成果報告書
• 掲載ページ: 1-5
• 本文の言語コード: jpn
• 件名標目: 仕様記述・仕様検証; 形式手法; ソフトウェア工学; 代数仕様; 証明スコア; CafeOBJ; 定理証明
• 対象利用者: 一般
• 一般注記: 仕様検証法の最重要課題として(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; 研究分野：形式手法、仕様検証、ソフトウェア工学; identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/13692
• オンライン閲覧公開範囲: 限定公開
• 連携機関・データベース: 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• 提供元機関・データベース: 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ