VDMTools: advances in support for formal modeling in VDM (2008)

Author(s): Fitzgerald JS, Larsen PG, Sahara S

    Abstract: We describe the current status of "VDMTools", a group of tools supporting the analysis of system models expressed in the formal language of the Vienna Development Method. Three dialects of the language are supported: the ISO standard VDM specification language with support for modular structuring, the extension VDM++ which supports objectoriented structuring and concurrency, and a version extending VDM++ with features for modeling and analysing distributed embedded real-time systems. VDMTools provides extensive static semantics checking, automatic code generation, roundtrip mapping to UML class diagrams, documentation support, test coverage analysis and debugging support. The tools’ focus is on supporting the cost-effective development and exploitation of formal models in industrial settings. The paper presents the components of VDMTools and reports recent experience using them for the development of large models.

      • Date: February 2008
      • Journal: ACM SIGPLAN Notices
      • Volume: 43
      • Issue: 2
      • Pages: 3-11
      • Publisher: Association for Computing Machinery
      • Publication type: Article
      • Bibliographic status: Published

      Keywords: Formal Methods, Vienna Development Method, VDM, Validation, Tool support

      Staff

      Professor John Fitzgerald
      Director of Research in Computing Science, Director of the Centre for Software Reliability