Alloy Analyzerを用いた表明に関する欠陥の検出手法 : JMLによる表明記述に対して

森, 恵弥佳; 岡野, 浩三; 楠本, 真二

コンピュータ ソフトウェア, 2013, 30(3), 187-193

Number of Access:912（2025-12-09 11:09 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/51342

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
Computer Software_30_3_187 pdf None 377 KB 197 2015.04.07 出版社版/publisher  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
Alloy Analyzerを用いた表明に関する欠陥の検出手法 : JMLによる表明記述に対して
A Method with Alloy Analyzer for Detecting Defects of Specifications : For JML Annotations
Alloy Analyzer　ヲ　モチイタ　ヒョウメイ　二　カンスル　ケッカン　ノ　ケンシュツ　シュホウ　JML　二　ヨル　ヒョウメイ　キジュツ　二　タイシテ
Creator
CreatorName
森, 恵弥佳 ; モリ, エミカ ; Mori, Emika
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
CreatorName
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
Description
森 恵弥佳, 岡野 浩三, 楠本 真二. Alloy Analyzerを用いた表明に関する欠陥の検出手法 ーJMLによる表明記述に対してー. コンピュータソフトウェア 30(3), 187 (2013); https://doi.org/10.11309/jssst.30.3_187.
Abstract
ソフトウェア開発の重要概念である契約による設計では，各クラス・メソッドが満たすべき仕様を表明として明確に定義することでソフトウェアの仕様理解の補助や，プログラム検証を可能にする．また表明の記述が十分であれば，メソッドの使用者が実装の詳細を考慮する必要がなくなり，情報隠蔽の度合いやモジュール性を高めることができる．しかし，表明の記述が不十分であったり表明と実装とが対応していないなどの欠陥があれば，これらの利点が十分に発揮されない．本研究では，Javaのソースコード中に表明を記述するための言語であるJMLの記述に対して，表明に関する欠陥を検出あるいは発見しやすくする手法を提案する．提案手法では，オブジェクト指向モデリングに影響を受けた形式仕様記述言語であるAlloyとその自動解析ツールAlloy Analyzerを利用した．また，ソフトウェア開発のための古典的な共通問題である在庫管理プログラムに対して適用実験を行った．その結果，8ヶ所の表明に関する欠陥を検出することができ，提案手法の有用性を確認できた．
Design by Contract (DbC) is one of key concepts of software development. According to the concept, designers explicitly define each class or method specification as assertion to be satisfied. It has the following advantages. First, it helps to understand the software specification and to verify the program. Secondly, sufficient description of assertion for a method helps users understand behavior of the method without the details of the implementation. Finally, it enhances information hiding and modularity. Defect that description of assertions is insufficient or inconsistency between specification and implementation, however, sometimes counteracts these advantages. This study proposes a method to detect and to help users find defects of specifications described by JML (Java Modeling Language). Our method utilizes Alloy Analyzer. An application experiment has been performed on a ware-house management program, which is the famous common problem for software development. As a result, eight defects of the assertion were detected. We can thus sure the effectiveness of this method was confirmed.
Publisher
日本ソフトウェア科学会
ニホン　ソフトウェア　カガクカイ
Japan Society for Software Science and Technology
Source Title
コンピュータ ソフトウェア
Volume (Issue)
30(3)
Page
187-193
Date of Issued
2013
Language
Japanese
Handle URL
https://hdl.handle.net/11094/51342
PISSN
02896540
Relation.isIdenticalTo
DOI (Publisher Version)
https://doi.org/10.11309/jssst.30.3_187
Access Rights
open access
CopyRight
ここに掲載した著作物の利用に関する注意 本著作物の著作権は日本ソフトウェア科学会に帰属します．本著作物は著作権者である日本ソフトウェア科学会の許可のもとに掲載するものです．ご利用に当たっては「著作権法」に従うことをお願いいたします．
Notice for the use of this material: The copyright of this material is retained by the Japan Society for Software Science and Technology (JSSST). This material is published on this web site with the agreement of the JSSST. Please be complied with Copyright Law of Japan if any users wish to reproduce, make derivative work, distribute or make available to the public any part or whole thereof.
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article