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

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

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

アクセス数:881件（2025-08-16 09:40 集計）

固定URL: https://hdl.handle.net/11094/51342

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
Computer Software_30_3_187 pdf なし 377 KB 171 2015.04.07 出版社版/publisher  

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル
Alloy Analyzerを用いた表明に関する欠陥の検出手法 : JMLによる表明記述に対して
A Method with Alloy Analyzer for Detecting Defects of Specifications : For JML Annotations
Alloy Analyzer　ヲ　モチイタ　ヒョウメイ　二　カンスル　ケッカン　ノ　ケンシュツ　シュホウ　JML　二　ヨル　ヒョウメイ　キジュツ　二　タイシテ
著者
著者名
森, 恵弥佳 ; モリ, エミカ ; Mori, Emika
NRID
1000070252632 1000070252632
著者名
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
著者名
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
内容
森 恵弥佳, 岡野 浩三, 楠本 真二. Alloy Analyzerを用いた表明に関する欠陥の検出手法 ーJMLによる表明記述に対してー. コンピュータソフトウェア 30(3), 187 (2013); https://doi.org/10.11309/jssst.30.3_187.
抄録
ソフトウェア開発の重要概念である契約による設計では，各クラス・メソッドが満たすべき仕様を表明として明確に定義することでソフトウェアの仕様理解の補助や，プログラム検証を可能にする．また表明の記述が十分であれば，メソッドの使用者が実装の詳細を考慮する必要がなくなり，情報隠蔽の度合いやモジュール性を高めることができる．しかし，表明の記述が不十分であったり表明と実装とが対応していないなどの欠陥があれば，これらの利点が十分に発揮されない．本研究では，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.
出版者
日本ソフトウェア科学会
ニホン　ソフトウェア　カガクカイ
Japan Society for Software Science and Technology
収録物名
コンピュータ ソフトウェア
巻(号)
30(3)
ページ
187-193
刊行年月
2013
言語
日本語
ハンドルURL
https://hdl.handle.net/11094/51342
PISSN
02896540
関連情報 (isIdenticalTo)
DOI (出版社版)
https://doi.org/10.11309/jssst.30.3_187
アクセス権
open access
権利情報
ここに掲載した著作物の利用に関する注意 本著作物の著作権は日本ソフトウェア科学会に帰属します．本著作物は著作権者である日本ソフトウェア科学会の許可のもとに掲載するものです．ご利用に当たっては「著作権法」に従うことをお願いいたします．
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.
出版タイプ
Version of Record
カテゴリ
学術雑誌論文 Journal Article