Welcome to the VDM Portal

VDM (The Vienna Development Method) is a set of techniques for modelling computing systems, analysing those models and progressing to detailed design and coding. VDM has its origins in the work of the IBM Vienna Laboratory in the mid-1970s. The notations and tools have steadily developed and are now applied on a wide range of systems. The aim of this portal is to provide 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. Dines Bjørner (one of VDM's inventors) gave an overview presentation about VDM including its history of more than thirty years. The latest VDM Flyer gives recent news and information in brief.

Latest News

February 2009: The call for papers for the Overture workshop to be held at the FM'09 conference is now on-line

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.

Industrial Uptake of Formal Methods In September 2007 Peter and John gave a short paper on industrial uptake of formal methods, based on the VDM experience, as part of the Festschrift in honour of Dines Bjørner and Zhou Chaochen in Macau. The essay is available in the Festschrift Volume. Technical reports on the subject are available here and here.

Japan Seminar Series In July 2007 two seminars on industrial use of VDM were held in Japan. The slides are available:

• Peter Gorm Larsen: Why use VDM and what are the future VDMTools development possibilities?
• Marcel Verhoef: Modelling and Analysis of Distributed Embedded Real-time Systems using VDM++ and VDMTools

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 examples

Members of the VDM community around the world have produced VDM models that they are willing to share with others. These are gathered as examples for both the VDM-SL notation and the VDM++ notation. For those unaware of VDM++ a quick overview is present.

VDM Tool Support

A number of different tools support VDM:

• 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. A tutorial providing a practical introduction to the different features of VDMTools and tools it connects to 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 CORBA support. Please contact VDM.SP@csk.com for any queries related to licensing.
• VDMTools have a CORBA-based Application Programmers Interface (API). Assistance about how to use this can be found here.
• Overture: is a community-based open source initiative aimed at providing freely available tool support for VDM++ 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.
• 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!

VDM Strategic Research Agenda

In line with the pan-European Joint Technology Platforms the core of the VDM community decided at the third Overture workshop to establish a strategic research agenda with the most important reseach issues that there is an agreement should be carried out during the next years. It is intended that this strategic research agenda will be refined as progress is made.

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 bibliogaphy 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.
• "Proof in VDM: A Practitioners Guide" Juan C. Bicarregui, John S. Fitzgerald, Peter A. Lindsay, Richard Moore and Brian Ritchie, Springer-Verlag, 1994, ISBN:0-387-19813-X.
• "Systematic Software Development using VDM" by Cliff Jones: This text is focusses on the use of VDM as a disciplined approach to software development, including the use of refinement and proof. Both the book and teaching notes can be found here.
• "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 - 19 Apr 2009