Welcome to the VDM Portal

VDM (The Vienna Development Method) is a set of techniques for modelling computing systems, analysing models and progressing to detailed design and coding. Since its origins in the IBM Vienna Laboratory in the mid-1970s, VDM's notations and tools have developed and are now applied on a wide range of systems. This portal provides pointers to all the material available on the web relevant for the VDM community.

If you would like a brief introduction to VDM, take a look at the Wikipedia entry or read Dines Bjørner's overview. The latest VDM Flyer gives recent news and information in brief.

Latest News

For all the latest news on VDM, visit the new Overture project site!

Older news:

January 2010: The DESTECS project has started. Over the next three years, the project will examine the potential of using VDM in distributed control applications. We focus on co-simulation technology as a way of allowing models of control software (in VDM) to be developed concurrently with models of the controlled plant or environment.

November 2009: A guided tour introducing Overture to new VDM++ users is now available. It serves as as a replacement for the tools introduction chapter (Chapter 3) in the VDM++ book.

November 2009: Materials from the 7th Overture Workshop held at FM 2009 in Eindhoven, the Netherlands, are now on-line. The proceedings of the workshop are available as a technical report from Newcastle University.

May 2009: Materials from the 6th Overture workshop, held on 7-8 May 2009 at Newcastle University, are now on-line . The workshop focussed on encouraging tools development.

The fifth VDM/Overture workshop took place on 8-9 November 2008 at the University of Minho in Braga, Portugal.

Jose Nuno Oliveira is leading a new group working on the Verified File Store (Posix) challenge.

The Fourth VDM/Overture Workshop took place on 26 May in Turku, as part of FM'08. You can read the proceedings on our workshops page.

VDM community

The VDM Forum is a free email based newsgroup for anyone interested in VDM. It's a great way to share and exchange experiences using VDM, and it's moderated to keep it free of spam.

VDM Tool Support

Several tools are available to support VDM:

• Overture: is a community-based open source initiative aimed at providing freely available tool support for all 3 VDM dialects (VDM-SL, VDM++ and VDM-RT) on top of the Eclipse platform. Its aim is to develop a framework for interoperable tools that will be useful for industrial application, research and education.

• VDMTools are the leading commercial tools for VDM and VDM++. You can download all documentation and executables when registered at the VDMTools site. The latest manuals are also available. VDMTools is owned, marketed, maintained and developed by CSK Systems, building on earlier versions developed by the Danish Company IFAD. Versions are available for Windows 2000/XP, Mac (G4, G5 and x86) and Linux. Tutorials for the different VDM dialects providing a practical introduction to the different features of Overture is available. All licenses are available, 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 a CORBA-based Application Programmers Interface (API, details at ). Please contact VDM.SP@csk.com for any queries related to licensing.

• SpecBox: from Adelard provides syntax checking, some simple semantic checking, and generation of a LaTeX file enabling specifications to be printed in mathematical notation. This tool is freely available but it is not being further maintained.

• LaTeX and LaTeX2e macros are available to help you write VDM-SL specifications in the ISO Standard Language's mathematical syntax. They have been developed and are maintained by the National Physical Laboratory in the UK. Read the README and get the downloads from here. You will need a large version of TeX to use the macros in any serious way. The contact at NPL is Graeme I Parkin, (Graeme.Parkin@npl.co.uk).

• Free editor for VDM++ with syntax highlighting that easily can be changed with different colour codings for keywords.

Grand Challenges in Computer Science : Dependable Systems Evolution

Groups of VDM enthusiasts are taking the initiative to participate in the GC6 project. Currently,

• JoseOliveira is leading a group working on the Verified File Store (Posix) challenge.
• JeremyBryans is leading the effort to work on the Mondex mini-challenge.
• HugoMacedo is leading the effort to work on the Pacemaker mini-challenge.

You can get an overview of all three studies by looking at John Fitzgerald's presentation from the Grand Challenges Workshop at FM'08.

You are welcome to join all three efforts!

The VDM Research Agenda

We maintain a research agenda which identifies the most significant or urgent research priorities identified by VDM community for the next 5 years.

VDM publications

VDM has been a major tool in research into rigorous and formal methods of software development. Many books, articles, workshops and conferencess have been devoted to VDM and its many aspects. A bibliography in bibtex format is available for VDM and a subset of that specifically for VDM++. An overview including VDM workshops and a collection of selected publications are available.

VDM teaching material

Several books about VDM have teaching material associated with them:

• "Validated Designs for Object-oriented Systems" by John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef: This is the newest book about VDM and here the VDM++ version is used in conjunction with UML. Course material can be found here.
• "Modelling Systems: Practical Tools and Techniques for Software Development" by John Fitzgerald and Peter Gorm Larsen: This book is about modelling using a subset of VDM-SL with a lot of focus on practical tool support. Course material can be found here.
• "Systematic Software Development using VDM" by Cliff Jones, 2nd edn., Prentice Hall 1990. This text is focusses on the use of VDM as a disciplined approach to software development, including the use of refinement and proof. Teaching material is also available.
• "Formal Software Development: From VDM to Java" by Quentin Charatan and Aaron Kans: The book introduces the VDM specification language by way of examples and also looks at the translation of these examples into Java. Teaching material can be found here.

-- JohnFitzgerald - 05 Jul 2010