軽量形式手法の一つ。仕様をモデルとして記述し検証するシステム。定義したデータの関係がどうなるか、模擬試験した結果を順に表示する仕組みがある。 設計者が想定していない関係が現れたら、仕様記述の不具合の可能性がある。 UML記述システムとAlloy Analyzeとの連携ソフトウェアがあり、UMLの記述ができる技術者が容易に利用できるようになっている。
脚注
参考文献
- 抽象によるソフトウェア設計−Alloyではじめる形式手法 ,Daniel Jackson, オーム社,2011年 ISBN 978-4274068584
- 在庫管理プログラムに対するAlloy Analyzerを用いた検証事例, 森 恵弥佳, 岡野浩三, 楠本真二,大阪大学, コンピュータソフトウェア, volume 30, number 3, pages 187-193 2013年8月.日本ソフトウェア科学会 http://sdl.ist.osaka-u.ac.jp/pman/pman3.cgi?DOWNLOAD=201
- 独立行政法人情報処理推進機構 委託 2013 年度ソフトウェア工学分野の先導的研究支援事業 「形式仕様とテスト生成の部分的・段階的な活用 ~探索を通したコード中心インクリメンタル型開発の支援」 成果報告書 平成 27 年 2 月 情報・システム研究機構 国立情報学研究所 https://www.ipa.go.jp/files/000045270.pdf
- 演習コースII 形式手法と仕様記述 Bチーム 2015/2/27 発表資料 蛸島 昭之, 日本科学技術連盟, http://juse-sqip.jp/workshop/seika/2014/attachs/20150227-II-B.pdf
外部リンク
- http://alloy.mit.edu/alloy/ alloyの配布元
