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:
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,
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