VDM Publications

Introductions to VDM with Tool Support

• John Fitzgerald and Peter Gorm Larsen, Modelling Systems: Practical Tools and Techniques for Software Development, Cambridge University Press 2nd Edition in English 2009, 1st Edition in Japanese 2003, 1st Edition in English 1998. This book also has course material available including slides in Japanese.

• 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.

Technical Books

• Juan C. Bicarregui, John S. Fitzgerald, Peter A. Lindsay, Richard Moore and Brian Ritchie, Proof in VDM: a Practitioner's Guide, Springer-Verlag, 1994, ISBN:0-387-19813-X. This book is still the most comprehensive guide to the proof theory underpinning VDM using the Typed Logic of Partial Functions. A PDF of the text is freely available on-line.

• Juan C. Bicarregui (ed.) Proof in VDM: Case Studies Springer-Verlag, 1998. This edited collection supports the "Proof in VDM" book by offering a series of case studies showing the application of rigorous proof in a range of applications and addressing the first steps towards automated proof support for VDM. A PDF of the text is freely available on-line.

• Cliff Jones, Systematic Software Development using VDM, Prentice Hall 1990. PDF files of the text and teaching material are freely available on-line.

• "Formal Software Development: From VDM to Java" by Quentin Charatan and Aaron Kans: This gently-paced introduction to software engineering and formal methiods uses VDM by way of examples and also looks at the translation of VDM into Java. Teaching material can be found here.

Recent Technical Papers and Theses

• Formal Semantics of a VDM Extension for Distributed Embedded Systems, Jozef Hooman and Marcel Verhoef, in D. Dams and U. Hannemann and M. Steffen (eds): W.P. de Roever Festschrift, LNCS 5930, pp 142-161, 2010.

• K. Lausdahl and H. K. Lintrup and P. G. Larsen, Connecting UML and VDM++ with Open Tool Support, in A. Cavalcanti and D. Dams (Eds.), FM 2009: Formal Methods, Procs. Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009, LNCS 5850, Springer 2009.

• P. G. Larsen, J. S. Fitzgerald and S. Wolff, Methods for the Development of Distributed Real-Time Embedded Systems using VDM, International Journal of Software and Informatics, 3(2-3),pp. 305-343, 2009. (Previously CS-TR 1164, School of Computing Science, Newcastle University)

• Taro Kurita, Yasumasa Nakatsugawa. The Application of VDM to the Industrial Development of Firmware for a Smart Card IC Chip. International Journal of Software and Informatics, 2009,3(2-3), pp. 343-355, 2009

• P. G. Larsen, J. S. Fitzgerald and S. Riddle. Practice-oriented courses in formal methods using VDM++, Formal Aspects of Computing 21(3), Springer-Verlag, 2009 DOI 10.1007/s00165-008-0068-5

• M. Verhoef, Modeling and Validating Distributed Embedded Real-Time Systems, PhD Thesis, Radboud University Nijmegen, 21 January 2009.

• J. S. Fitzgerald, P. G. Larsen and M. Verhoef, Vienna Development Method, in B. Wah (ed.), Wiley Encyclopedia of Computer Science and Engineering, John Wiley & Sons. ISBN 0471383937, September 2008.

• J. S. Fitzgerald, J. W. Bryans, D. Greathead, C. B. Jones and R. Payne, Animation-based Validation of a Formal Model of Dynamic Virtual Organisations, in P. Boca, J. P. Bowen and P. G. Larsen (eds.) Proc. BCS-FACS Workshop on Formal Methods in Industry, Electronic Workshops in Computing, The British Computer Society, 2008.

• John Fitzgerald, Peter Gorm Larsen and Shin Sahara, VDMTools: advances in support for formal modeling in VDM, ACM SIGPLAN Notices 43(2), February 2008. (Previously Technical Report CS-TR-1057, School of Computing Science, Newcastle University)

• P. G. Larsen and J. S. Fitzgerald. Recent Industrial Applications of VDM in Japan, in P. Boca, J. P. Bowen and P. G. Larsen (eds.) Proc. BCS-FACS Workshop on Formal Methods in Industry, Electronic Workshops in Computing, The British Computer Society, 2008.

• Hugo Daniel Macedo, Peter Gorm Larsen and John Fitzgerald, Incremental Development of a Distributed Real-Time Model of A Cardiac Pacing System using VDM, in Jorge Cuellar and Tom Maibaum (Eds.), FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Lecture Notes in Computer Science Vol. 5014, ISBN: 9783540682356, May 2008 (Previously Technical Report CS-TR-1059, School of Computing Science, Newcastle University).

• J. S. Fitzgerald and C. B. Jones. The Connection between Two Ways of Reasoning about Partial Functions, The Connection between Two Ways of Reasoning about Partial Functions, Information Processing Letters 107(3-4), pp. 128-132, 2008 (Previous version was Technical Report CS-TR-1044, 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.

• Zoe Andrews, John Fitzgerald, Marcel Verhoef. Resilience Modelling Through Discrete Event and Continuous Time Co-Simulation, in Proc. 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (July 2007).

• 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.

Conferences and Workshops about VDM

We hold frequent and informal Overture Workshops that include reports on all aspects of VDM, including industry and academic applications, fundamental research, tools development and use, and experience gained in teaching and learning. More mature work is published in journals and books.

The first major conferences on VDM were organised by the VDM Europe between 1987 to 1991. When VDM Europe 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 are published in conferences and journals, but work in progress has also been reported in the less formal VDM and Overture Workshop series that started in 1999. These include:

• The First VDM Workshop, 21-22 Sept. 1999 in Toulouse, France, as part of FM'99
• The Second VDM Workshop 2 Sept. 2000 in York, UK, as part of ZB 2000
• The Third VDM Workshop 20-22 July 2002 in Copenhagen, Denmark, as part of FME 2002.

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 - 28 Dec 2009