, 仕様記述言語JMLとAlloy を用いた在庫管理プログラムの設計に対するモデル検査ツールによる検証事例, 2007.
ID 25
分類 学位論文
タグ case study design warehouse management program jml alloy verification validation tools
キー (key) Masayuki Owashi
URL
注釈 (annote)
内容梗概 (abstract) ソフトウェアの開発において,従来から使われている手法としてV字型モデルによる設計法がある.このV字型設計法において,近年,Design by Contract(契約に基づく設計,以下DbCとする)による考え方が脚光を浴びている.DbCに基づいた開発では,アサーションにより契約を示す.アサーションを実現するための言語のとしてAlloyやJMLが挙げられる.Alloyは,Model Finderと呼ばれるAlloyAnalyzerを用いて,抽象度の高い設計において,仕様の矛盾発見などに役立つ.一方JMLは,Javaコードと結びついており,抽象度の低い段階での設計,実装の検証に役立つ.このため,AlloyからJMLに変換が可能ならば,抽象度が高く正当性のある程度保障された契約に対し,それ侵さぬよう低レベル設計が得られるため,より信頼性の高い開発を行うことができる.

本研究では,AlloyからJML付きのJavaのコードへの変換をすることを念頭において,そのための事例研究として,在庫管理プログラムの設計をAlloyとJMLで行った.それぞれAlloyAnalyzerとESC/Javaを用いてその正当性を検証した.また,各検証については,作成した在庫管理プログラムにおいて,警告内容について,なぜそのような警告がでたか,そして解決できたかについてまとめ考察した.結果,Alloyにおいては一部仕様を省略したがAlloyによる述語の扱い方を工夫することによりJMLと類似した記法により仕様記述をすることができた.

論文電子ファイル 0 (application/pdf) [一般閲覧可]
BiBTeXエントリ
@bachelorthesis{id25,
}