SCSK株式会社が上記公式URLを開始しましたので、このページ内の「公式」情報は、徐々に上記へ移行する予定です。
VDM情報 | VDM++教科書 | Overture Project
CSK VDMToolsは、ISO標準のVDMを拡張した形式仕様記述言語VDM-SLと、そのオブジェクト指向拡張であるVDM++による、分析・設計・開発を支援する実用性の高い統合ツールです。2005年、（株）CSKシステムズがデンマークの会社から全ての権利を買い取り、100倍高速化し、ライセンス契約のもとに無料で提供しています。
ツールやマニュアルのダウンロード方法詳細は、VDMTools公式ページをご覧ください。
VDMToolsはすでに産業界と大学で広く使われており、日本の鉄道総合技術研究所・フェリカネットワークス・SCSK・九州大学・国立情報学研究所 北陸先端科学技術大学院大学や、米国ロックウェル社、英国ロールスロイス社、フランスのダッソー社、オランダ国防省などがユーザーになっています。
CSK VDMToolsは、形式技術と実用技術を巧みに統合し、現在は以下の機能を提供します。
稼働環境は以下の通りです。
No. 5 (2000年11月) 日本語版
鉄道総合研究所(RTRI)と日本フィッツ(JFITS)
No.5 English Version
日本語版VDM++入門コース
英語版VDM++入門コース
パンフレット
製品パンフレットです。
RoseLink
ラショナル社のRational Roseとのリンク機能nいついての説明です。
確認済設計
確認済設計によるモデル化のためのVDMToolsnいついての説明です。
オランダ国防省の事例
オランダ国防総省の事例報告です。
佐原伸, 形式手法の技術講座―ソフトウェアトラブルを予防する、SRC、2008年５月
形式手法VDM++の入門書であり、また、形式手法の比較も行っています。
ジョン・フィッツジェラルド，ピーター・ゴーム・ラーセン著: 荒木 啓二郎，張 漢明，荻野 隆彦，佐原 伸，染谷 誠 訳､ソフトウェア開発のモデル化技法, 岩波書店, 2003, ISBN4-00-005609-3 C3004
下記の本の翻訳で、理論面より実際のモデル構築に重点を置いたVDM-SLの入門用教科書です。
John Fitzgerald, Peter Gorm Larsen. Modelling Systems: Practical Tools and Techniques for Software Development. Cambridge University Press, 1998, ISBN 0521 62348 0
荒木啓二郎, 張漢明: プログラム仕様記述論, 2002, ISBN4-274-13263-3, オーム社出版局
形式手法の基本に重点を置いた、入門用教科書です。
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M. : Validated Designs for Object-oriented Systems, Springer, 2005, ISBN: 1-85233-881-4
上記の本の著者達による、理論面より実際のモデル構築に重点を置いたVDM++の入門用教科書です。
この本の例題その他の情報URLから、VDMTools非商用版のダウンロードができる。
CLIFF B JONES, SYSTEMATIC SOFTWARE DEVELOPMENT USING VDM SECOND EDITION, Prentice Hall International,1990
VDMの元祖の一人、Jonse教授の有名な教科書の第２版がダウンロードできます。
佐原伸, 事務処理用VDM++フレームワークの作成, ソフトウェア・シンポジウム2004
事務処理システムの要求定義に使用したVDM++用フレームワークについての論文です。
佐原伸, VDM++基本ライブラリの作成, ソフトウェア・シンポジウム2004
VDM++用に作成した基本ライブラリについての論文です。
佐原伸, VDM++関数型回帰テスト支援ライブラリ, ソフトウェア・シンポジウム2005
最初、オブジェクト指向で作成したVDM++用の回帰テスト支援ライブラリを、関数型プログラミング技法を使って改良し、テストケース行数を減らした経験とそのソース。
佐原伸, 事務システムにおける形式仕様適用例, ソフトウェア・シンポジウム2001
VDM++を実システム開発に用いた経験を述べた論文です。
佐原伸, 事務システムにおける形式仕様適用例OHP, ソフトウェア・シンポジウム2001
上記論文の発表時のOHPです。