VDMTools

"Validated Designs for Object-oriented Systems" is supported by high quality industry-strength tools owned and marketed by CSK Systems Corporation of Japan. The full functionality includes model syntax- and type-checking, an interpreter, test coverage support, proof obligation generation, code generation for C++ and Java, the link to Rose, and much more. Platforms supported include Linux, Windows, MacG4^?/5. For full details of the tools visit http://www.vdmtools.jp/en. The following versions are available for download:

• VDMTools Lite: This limited-functionality version is available for non-commercial use. It is designed for readers of the "Validated Designs" book wishing to attempt the exercises and those wishing to explore the tool support available for VDM models. Download directly from http://www.vdmtools.jp/en (Free of charge, but you will need to register).

• Academic Version: This full-functionality version is available free of charge to academic users, for non-commercial research and teaching purposes. To request this version, please email VDM.SP@csk.com.

• Commercial Version: The full-functionality tools are available from CSK. To request this version, please email VDM.SP@csk.com.

Documentation is available from http://www.vdmtools.jp/en