VDM Publications

Recent Publications

• John S. Fitzgerald and Cliff B. Jones. The Connection between Two Ways of Reasoning about Partial Functions, TR1044, School of Computing Science, Newcastle University, Aug 2007 (PDF). This paper discusses the relationship between two logics that provide alternative ways of reasoning about partial functions. Theorems in the Logic of Partial Functions using weak equality (the logic on which VDM is based) can be directly translated into First Order Predicate Calculus using existential equality. Translation in the other direction is, in general, more complicated but simplifies pleasingly in many cases. Such results are important if formal methods tool integration is to be done safely.

• Marcel Verhoef and Peter Gorm Larsen. Interpreting Distributed System Architectures using VDM++ – A Case Study, in R. Jain, B Stevens, G. Müller (eds.), Proc. 5th Annual Conference on Systems Engineering Research, March 14-16, 2007. (PDF) This provides an overview of the system engineering capabilities in the new extensions of VDM++ enabling the description and analysis of real-time, distributed systems.

• John S. Fitzgerald, Peter Gorm Larsen, Simon Tjell and Marcel Verhoef. Validation Support for Distributed Real-Time Embedded Systems in VDM++, to appear in Proc. 10th IEEE High Assurance Systems Engineering Symposium, Dallas, Texas, Nov. 2007. Revised Version of TR1017, School of Computing Science, Newcastle University, Apr 2007 (PDF). A new facility is proposed for stating and checking validation conjectures against traces derived from the execution of scenarios on VDM++ models. We describe the implementation of conjectures against execution traces as a formally-defined extension to the existing VDM++ tool set, and show tools to support the visualisation of traces and validation conjecture violations.

• Jeremy W. Bryans and John S. Fitzgerald. Formal Engineering of XACML Access Control Policies in VDM++, to appear in Proc. 9th International Conference on Formal Engineering Methods, Florida Atlantic University, Boca Raton, Florida, USA, November 2007. Also TR 1028, School of Computing Science, Newcastle University, Jan 2007 (PDF). This provides an introduction to the VDM++ semantics of the eXtensible Access Control Markup Language. Abstractions in the model are potentially very useful in understanding the problems of managing access control in virtual organisations.

• Marcel Verhoef, Peter Gorm Larsen and Jozef Hooman. Modeling and Validating Distributed Embedded Real-Time Systems with VDM++", Springer Verlag Berlin, in FM 2006: Formal Methods, ISBN 3-540-37215-6, August 2006. (PDF). This provides the semantics and a small case study of new extensions for VDM++ enabling the description and analysis of real-time, distributed systems.

• John Fitzgerald and Peter Gorm Larsen. Triumphs and Challenges for the Industrial Application of Model-Oriented Formal Methods, to appear in T. Margaria, A. Philippou and B. Steffen (eds.), Proc. 2nd Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), IEEE 2007. Also TR999, School of Computing Science, Newcastle University, Jan 2007 (PDF). This gathers brief details of many of the significant industry applications of VDM and VDM++ in recent years. We compare the tools-based approach of VDM with the vision of "lightweight" formal methods first advocated in the mid-1990s.

• Jeremy Bryans, John Fitzgerald, Cliff Jones, Igor Mozolevsky. Formal Modelling of Dynamic Coalitions, with an Application in Chemical Engineering, to appear in T. Margaria, A. Philippou and B. Steffen (eds.), Proc. 2nd Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), IEEE 2007. Also TR981, School of Computing Science, Newcastle University, Sep 2006 (PDF). Describes the lightweight use of VDM to map out a space of dynamic coalitions (dynamically changing collections of cooperating agents which share information and work towards a common goal). The models developed are adapted to a real DC in the chemical engineering industry.

• John Fitzgerald, Peter Gorm Larsen and Steve Riddle. Learning by Doing: Practical Courses in Lightweight Formal Methods using VDM++. TR 992, School of Computing Science, Newcastle University, Dec 2006 (PDF). This paper describes the practical approaches to teaching VDM and VDM++ used at Aarhus and Newcastle. It is developed from Peter Gorm Larsen's presentation at the FM06 workshop on Formal Methods Education.

• John Fitzgerald. The Typed Logic of Partial Functions and the Vienna Development Method. To appear in Dines Bjorner and Martin Henson (eds.) Logics of Specification Languages, Springer Monographs in Theoretical Computer Science (EATCS Series), 2007, pages 427-461. Also TR 984, School of Computing Science, Newcastle University, Oct 2006 (PDF). A technical discussion of the use of the non-Classical Logic of Partial Functions (LPF) to underpin reasoning about VDM models. The paper concentrates on the implementation of the typed form of LPF.

• Jeremy Bryans, John Fitzgerald and Panos Periorellis. Model Based Analysis and Validation of Access Control Policies, TR 976, School of Computing Science, Newcastle University, July 2006 (PDF). A first VDM formalisation of XACML-based access control policies. The model is being developed further and applied to information security for dynamic coalitions.

Books about VDM

• John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat, Marcel Verhoef, Validated Designs for Object-oriented Systems, Springer Verlag 2005. This is the latest book on VDM and in particular its object-oriented extensions in VDM++. Course material supporting this book is also available.

• John Fitzgerald and Peter Gorm Larsen, Modelling Systems: Practical Tools and Techniques for Software Development, Cambridge University Press 1998, also has course material available even including slides in Japanese.

• Cliff Jones, Systematic Software Development using VDM, Prentice Hall 1990, now available on-line and free of charge and course material is also available.

Conferences and Workshops about VDM

The first major conferences on VDM were organised by the VDM Europe between 1987 to 1991. When VDMEurope widened its scope to incorporate all formal methods, the group changed its name to Formal Methods Europe and began the series of FME symposia. Now FME is an independent association and organises the leading series of "FM" conferences.

Papers about VDM have been published in conferences and journals, but work in progress has also been reported int heless formal VDM Workshop series that started in 1999. these include:

• The First VDM Workshop at FM'99 was held on 21-22 Sept. 1999 in Toulouse, France. We had one day of presentations on methodology, tools and education and one day entirely devoted to industrial application reports. Take a look at the presentations on the summary page.
• The Second VDM Workshop was held on 2 September 2000 as part of the ZB 2000 meeting at the University of York, UK.
• The Third VDM Workshop was held 20-22 July 2002 in Copenhagen, Denmark as part of the FME 2002 symposium.

These were followed by a series of workshops dedicated to the open source VDM project called Overture. You can find papers from the Overture Workshops at the Overture site.

VDM-SL ISO Standard

The VDM Specification Language achieved ISO Standardisation in 1996. The full bibliographic reference for the standard is:

Information technology -- Programming languages, their environments and system software interfaces -- Vienna Development Method -- Specification Language -- Part 1: Base language. International Standard ISO/IEC 13817-1, December 1996. Copies of the full standard my be ordered from The ISO Web site.

A Leicester University technical report describing the standard in detail is available. (PDF). Contact is Derek Andrews (derek.andrews@yahoo.com).

-- JohnFitzgerald - 16 Aug 2007