Home
Tool support
Example models
Chemical plant
(Chapter 2)
Alarm init
(Chapter 3)
Robot (Chapter 6) CWS (Chapter 7) CWS (Chapter 8) Enigma (Chapter 9) CSLaM (Chapter 10) POP3 (Chapters 12 and 13)
Solutions to exercises
Exercise 7.17
Errata Teaching VDM++ Related material Extra examples Contact

VDMTools

"Validated Designs for Object-oriented Systems" is supported by high quality industry-strength tools owned and marketed by CSK Corporation of Japan, the mother company to one of the successful VDM++ users (JFITS) whose experiences are described in the book. VDMTools is now available as follows.

Non-commercial Version (supporting the Validated Designs book)
This limited-functionality version is available to readers of the "Validated Designs" book wishing to attempt the exercises and those wishing to explore the tool support available for VDM models. This version (for Windows 2000/XP only) is available for direct download (22.2 Mbyte) from this web site. The following documentation is available (also included in the download):

For information on Rational Rose, click here

Academic Version
This full-functionality version is available to academic users, for non-commercial research and teaching purposes. To obtain a license and binaries, please email a request to VDM.SP@csk.com.

Commercial Version
The full-functionality tools are available on a commercial basis from CSK. Please email enquiries to VDM.SP@csk.com.

Overture

In addition to VDMTools, a new open source toolset supporting VDM++ is currently being developed. See The Overture project for more details.