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.
For all the latest news on VDM, visit the new Overture
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)
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
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
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 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:
- 05 Jul 2010