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

Material type: 文書・図像類

Author: 二木, 厚吉

Publisher: -

Publication date: 2016-05-18

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 仕様検証法の最重要課題として(1)適切な抽象度と(2)推論型×探索型検証を実現する技術の研究を、重要な仕様検証事例として(3)ソフトウェア自動更新と(4)車載OS標準の事例開発を、補完的に推進した。(1)-(4)の成果を、CafeOBJ仕様言語システムに統合することで、革新的仕様検証システムを実現し...

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

JAIST Repository
Digital
You can check the holdings of institutions and databases with which 学術機関リポジトリデータベース（IRDB）（機関リポジトリ） is linked at the site of 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）.
JAIST Repository

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

Material Type: 文書・図像類
Title: 証明スコア法に基づく革新的仕様検証システムの構築
Author/Editor: 二木, 厚吉
Author Heading: 二木, 厚吉
Publication Date: 2016-05-18
Publication Date (W3CDTF): 2016-05-18
Alternative Title: Development of the Innovative Specification Verification System based on Proof Scores
Periodical title: 科学研究費助成事業研究成果報告書
Pages: 1-5
Text Language Code: jpn
Subject Heading: 仕様記述・仕様検証
形式手法
ソフトウェア工学
代数仕様
証明スコア
CafeOBJ
定理証明
Target Audience: 一般
Note (General): 仕様検証法の最重要課題として(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
Format (IMT): application/pdf
Source: https://dspace.jaist.ac.jp/dspace/bitstream/10119/13692/1/23220002seika.pdf
https://dspace.jaist.ac.jp/dspace/bitstream/10119/13692/1/23220002seika.pdf
Access Restrictions: 限定公開
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ