Alloy Analyzer

軽量形式手法の一つ。仕様をモデルとして記述し検証するシステム。定義したデータの関係がどうなるか、模擬試験した結果を順に表示する仕組みがある。設計者が想定していない関係が現れたら、仕様記述の不具合の可能性がある。 UML記述システムとAlloy Analyzeとの連携ソフトウェアがあり、UMLの記述ができる技術者が容易に利用できるようになっている。^[1]

脚注

^ http://www.sparxsystems.jp/products/EA/tech/Alloy.htm UML記述システムとAlloy Analyzerとの連携

参考文献

抽象によるソフトウェア設計−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の配布元

[1] ttp://www.sparxsystems.jp/products/EA/tech/Alloy.htm UML記述システムとAlloy Analyzerとの連携

[1]