Validated Designs for Object-oriented Systems

This website complements the book Validated Designs for Object-oriented Systems. Here you can find sample models, solutions to exercises, course material and more information on the VDM++ modelling language and tools that support it. If you would like to know more about VDM we recommend visiting the VDM Portal. Since we are using TWiki, you can contribute to this site too!

About the book

Object-oriented design methods are commonplace in computing systems development, but are often dismissed as little more than 'boxes and arrows'. If systems developers are to gain the full advantage from such methods, they should be able to achieve designs that are not merely the subject of heated argument, but can be improved by careful, rigorous and machine-supported analysis. Validated Designs for Object-oriented Systems describes an object-oriented design approach that combines the benefits of abstract modelling with the analytic power of formal methods, to give designs that can be rigorously validated and assured with automated support. UML class models are augmented with consistent, complementary functional views in VDM++, with the engineer free to move between them. This allows developers to choose levels of abstraction and rigour appropriate to each given project. Aimed at software architects, designers and developers as well as computer scientists, no prior knowledge of formal methods is assumed. The elements of functional modelling are introduced using numerous examples and exercises, industrial case studies and experience reports. This book complements "Modelling Systems" by John Fitzgerald and Peter Gorm Larsen, now available in its second edition.

Tool support

CSK Systems has kindly provided a special version of VDMTools to support our book. VDMTools Lite is available free of charge and can be downloaded from www.vdmtools.jp/en. Versions are available for Windows 2000/XP, Mac (G4, G5 and x86) and Linux. For academic users, site licenses are available, also free of charge, for the full version of the tool. The full version includes automatic code generation for Java and C++, dynamic link library and CORBA support. Please contact VDM.SP@csk.com for any queries related to licensing.

The alternative to VDMTools is to use the Overture open source solution built on top of the Eclipse platform. A tutorial introducing Overture in a way similar to chapter 3 of the book can be downloaded. Overture stand-alone executables for Windows, Mac and Linux are also freely available.

Reference

Validated Designs for Object-oriented Systems. John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef. ISBN: 1-85233-881-4. Springer, New York. 2005. Download the BIB file entry vdmbook.bib.

You can purchase the book on-line at the Springer web-site. A Japanese translation is available as ISBN 978-1-85233-881-7 from August 2010, also available from the same publisher.

Course material

Slides supporting the book can be found on the VDM Portal.

Errata

Please have a look at our on-line Errata sheet. Found errors in the book? You are welcome to update this document!

Alternatively if you are looking for Payday Loans in the UK then look no further. Financial help when you need it