形式手法Alloyを用いた図式モデルのための段階的検証方法

Material type: 文書・図像類

Author: 寺中, 慎介 / 村上, 祥平 / 小飼, 敬 / 上田, 賀一ほか

Publisher: 情報処理学会

Publication date: 2008-03-17

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: application/pdfテクニカルレポート近年,ソフトウェアに対する信頼性や安全性に対する関心が高まり,形式手法が注目を集めている.形式手法に対する敷居の高さを解決するために,これまでにZ言語で記述された図式モデルを対象に形式手法に則った検証が行える形式手法支援ツールを実現してきた.本研究では...

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

Ibaraki University Academic Repository
Digital
You can check the holdings of institutions and databases with which Institutional Repositories DataBase(IRDB)(Institutional Repository) is linked at the site of Institutional Repositories DataBase(IRDB)(Institutional Repository).
Ibaraki University Academic 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: 形式手法Alloyを用いた図式モデルのための段階的検証方法
Author/Editor: 寺中, 慎介 / 村上, 祥平 / 小飼, 敬 / 上田, 賀一
TERANAKA, Shinsuke / MURAKAMI, Shohei / KOGAI, Kei / UEDA, Yoshikazu
Author Heading: 寺中, 慎介 / 村上, 祥平 / 小飼, 敬 / 上田, 賀一
TERANAKA, Shinsuke / MURAKAMI, Shohei / KOGAI, Kei / UEDA, Yoshikazu
Publication, Distribution, etc.: 情報処理学会
Publication Date: 2008-03-17
Publication Date (W3CDTF): 2008-03-17
Alternative Title: A Phased Verification Method for Diagrammatic Model Using Alloy
ケイシキシュホウ Alloy オモチイタズシキモデルノタメノダンカイテキケンショウホウホウ
Periodical title: 情報処理学会研究報告. ソフトウェア工学研究会報告
No. or year of volume/issue: 29
Volume: 29
Pages: 187-194
Text Language Code: jpn
Target Audience: 一般
Note (General): application/pdf
テクニカルレポート
近年,ソフトウェアに対する信頼性や安全性に対する関心が高まり,形式手法が注目を集めている.形式手法に対する敷居の高さを解決するために,これまでにZ言語で記述された図式モデルを対象に形式手法に則った検証が行える形式手法支援ツールを実現してきた.本研究では,この図式モデルを対象としたより実用的な形式仕様記述支援ツールについて模索する.方針として,既存の処理系としてライトウェイトな形式手法が実現できるAlloyに着目し,図式モデルに対する段階的な検証方法を提案する.また,検証例として DFDの階層化を行い,制約記述の方法や検証の性能評価について考察した.
In late years, the concern for reliability and safety to the software rises, and the formal method attracts attention. To solve the height of the threshold to the formal method, we had realized the formal method supporting tool, which could perform the verification of the formal specification for a diagrammatic model written in Z language. In this study, it seeks for a more practicable formal specification supporting tool for this diagrammatic model. As the policy, we pay our attention to Alloy which can realize a light-weighted formal method as an existing processing system, and propose a phased verification method for a diagrammatic model. Moreover, we hierarchize DFD as the verification example, and we consider the method and the performance of the verification of the restriction specification.
Access Restrictions: 限定公開
Rights (production): 情報処理学会
本文データは学協会の許諾に基づきCiNiiから複製したものである
Periodical Title (NCID): AN10112981
https://ci.nii.ac.jp/ncid/AN10112981
Is Version Of (URI): URI
http://ci.nii.ac.jp/naid/110006827764
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 茨城大学 : 茨城大学学術情報リポジトリ