Vienna Development Method

  • V. S. Alagar
  • K. Periyasamy
Part of the Texts in Computer Science book series (TCS)


The Vienna Development Method (VDM) is an environment for the modeling and development of sequential software systems. The specification language of VDM has evolved from Meta-IV, the language used at IBM’s Vienna development laboratory for specifying the semantics of the PL/I programming language in the early seventies. The current version of the VDM specification language, VDM-SL, has been standardized by the International Standards Organization (ISO). It supports the modeling and analysis of software systems at different levels of abstraction. Using VDM-SL constructs, both data and algorithmic abstractions expressed in one level can be refined to a lower level to derive a concrete model that is closer to the final implementation of the system.


Network Manager Proof Obligation Data Refinement Proof Rule Composite Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Agerholm S (1996) Translating specifications in VDM-SL to PVS. In: v. Wright J, Grundy J, Harrison J (eds) Proceedings of the international conference on theorem proving in higher order logics (TPHOL’96). Springer, Berlin Google Scholar
  2. 2.
    Andrews A, Ince D (1991) Practical formal methods using VDM. McGraw Hill, New York Google Scholar
  3. 3.
    Bicarregui JC et al. (1994) Proof in VDM: a practitioner’s guide. Springer, Berlin CrossRefGoogle Scholar
  4. 4.
    Bicarregui J, Ritchie B (1991) Reasoning about VDM developments using the VDM tool support in mural. In: Prehn S, Toetenel WJ (eds) VDM’91: formal software development methods. Lecture notes in computer science, vol 552. Springer, Berlin, pp 371–388 CrossRefGoogle Scholar
  5. 5.
    Bicarregui J, Matthews B (1995) Formal methods in practice: a comparison of two support systems for proof. In: Bartosek A et al. (eds) SOFSEM’95: theory and practice of informatics. Lecture notes in computer science, vol 1012. Springer, Berlin Google Scholar
  6. 6.
    Clement T (1994) Comparing approaches to data reification. In: Naftalin M, Denvir T, Bertran M (eds) FME’94: industrial benefits of formal methods. Lecture notes in computer science, vol 893. Springer, Berlin, pp 118–133 CrossRefGoogle Scholar
  7. 7.
    Clement T (1996) Data reification without explicit abstraction functions. In: Gaudel MC, Woodcock JCP (eds) FME’96: industrial benefits and advances in formal methods. Lecture notes in computer science, vol 1051. Springer, Berlin, pp 195–213 CrossRefGoogle Scholar
  8. 8.
    Cohen B, Harwood WT, Jackson MI (1986) The specification of complex systems. Addison-Wesley, Reading Google Scholar
  9. 9.
    Dawes J (1991) The VDM-SL reference guide. Pitman, London Google Scholar
  10. 10.
    Droschl G (1999) On the integration of formal methods: events and scenarios in PVS and VDM. In: Third Irish workshop on formal methods, Galway, Eire, July 1999 Google Scholar
  11. 11.
    Durr EH, Plat N (eds) (1995) VDM++: language reference manual, Afrodite (ESPRIT-III, project number 6500) document, Cap Volmac, Aug 1995 Google Scholar
  12. 12.
    Durr EH, Goldsack S (1996) Formal methods and object technology. In: Concurrency and real-time in VDM++. Springer, Berlin, pp 86–112 Google Scholar
  13. 13.
    Elvang-Goransson M (1991) Reasoning about VDM specifications. In: Prehn S, Toetenel WJ (eds) VDM’91: formal software development methods. Lecture notes in computer science, vol 552. Springer, Berlin, pp 343–355 CrossRefGoogle Scholar
  14. 14.
    Fitzgerald JS et al. (2007) Validation support for real-time embedded systems in VDM++. In: Proceedings of the 10th IEEE high assurance systems engineering symposium (HAS 2007), Nov 2007, pp 331–340 CrossRefGoogle Scholar
  15. 15.
    Goldsack SJ, Durr EH, Plat N (1995) Object reification in VDM++. In: Wirsing M (ed) ICSE-17: workshop on formal methods application in software engineering practice, April 1995, pp 194–201 Google Scholar
  16. 16.
    Goldsack S, Lano K (1996) Annealing and data decomposition in VDM. ACM SIGPLAN Not 31(4):32–38 CrossRefGoogle Scholar
  17. 17.
    Harry A (1996) Formal methods fact file: VDM and Z. Wiley, New York Google Scholar
  18. 18.
    Hekmatpour S, Ince D (1988) Software prototyping, formal methods and VDM. Addison-Wesley, Reading Google Scholar
  19. 19.
    The VDM-SL Tool Group (1995) User manual for the IFAD VDM-SL toolbox, IFAD, The Institute of Applied Computer Science, Forskerparken 10, DK-5230 Odense M, Denmark, June 1995 Google Scholar
  20. 20.
    Larsen PG et al. (1996) Information technology—programming languages, their environments and system software interfaces—Vienna development method—Specification language—Part 1: Base language. ISO document, December 1996 Google Scholar
  21. 21.
    Jones CB (1986) The systematic software development using VDM. Series in Computer Science. Prentice Hall International, Englewood Cliffs Google Scholar
  22. 22.
    Jones CB (1990) The systematic software development using VDM, 2nd edn. Series in computer science. Prentice Hall International, Englewood Cliffs Google Scholar
  23. 23.
    Jones CB, Jones KD, Lindsay PA, Moore R (1991) Mural: a formal development support system. Springer, Berlin MATHCrossRefGoogle Scholar
  24. 24.
    Jones CB, Shaw RC (1990) Case Studies in systematic software development. Series in computer science. Prentice Hall International, Englewood Cliffs MATHGoogle Scholar
  25. 25.
    Kurita T, Nakatsugawa Y (2009) The application of VDM++ to the development of firmware for a smart card IC chip. Int J Softw Informatics 3(2–3) Google Scholar
  26. 26.
    Larsen PG et al. (2010) The overture initiative—integrating tools for VDM. ACM Softw Eng Notes 35(1) Google Scholar
  27. 27.
    Ledru Y (1996) Using KIDS as a tool support for VDM. In: Proceedings of the 18th international conference on software engineering, March 1996, pp 236–245 Google Scholar
  28. 28.
    Lucas P (1987) VDM: origins, hopes and achievements. In: Bjorner D et al. (eds) VDM’87: VDM—a formal method at work. Lecture notes in computer science, vol 252. Springer, Berlin, pp 1–8 CrossRefGoogle Scholar
  29. 29.
    Mukherjee P et al. (2000) Exploring timing properties using VDM++ on an industrial application. In: Proceedings of the second VDM workshop, Sep 2000 Google Scholar
  30. 30.
    Parkin GI, O’Neil G (1991) Specification of the MAA standard in VDM. In: VDM’91: formal software development methods. Lecture notes in computer science, vol 552. Springer, Berlin, pp 526–544 CrossRefGoogle Scholar
  31. 31.
    Parkin GI (1994) Vienna development method specification language (VDM-SL). Comput Stand Interfaces 16:527–530 CrossRefGoogle Scholar
  32. 32.
    Pronk C, Schonhacker M (1996) ISO/IEC 10514-1, the standard for Modula-2: process aspects. ACM SIGPLAN Not 31(8):74–83 CrossRefGoogle Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.Dept. Computer Science and Software Eng.Concordia UniversityMontrealCanada
  2. 2.Computer Science DepartmentUniversity of Wisconsin-La CrosseLa CrosseUSA

Personalised recommendations