| Tweet | |
| , 仕様記述言語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,
}
|