The VDM++ Examples Repository

This page provides a series of substantial, examples of models produced using VDM++, all freely available. The authors have also made the VDM source available. So, if you are interested in taking an example further you can download the source (in UNIX file format).

If you have access to the one of VDM++ versions of VDMTools you can actually analyse the source texts further.

All postscript and pdf versions of the documents have been automatically generated from the source texts which have been submitted, unless the providers have explicitly produced the postscript output. Those who have submitted plain ASCII specifications have been included in a simple skeleton. Thus, some places the line breaks could be improved.

• Specification of a small Banking System : This VDM++ model contains 5 small classes that model the essentials of handling bank accounts and having credit cards that can draw money from such bank accounts.
• A Cash Dispenser System (Kim Sunesen, Sten Agerholm and Peter Gorm Larsen): This application example is a "Cash-point'' service system with tills and a central database for all the customers. The customers must use their PIN code when they extract money from their credit card and this is modeled both in VDM++ without taking concurrency and distribution into account and subsequently taking this into account. There is also an overall document that first provides an overview of the informal requirements from the system and then it proceeds with how such a problem could be dealt with using VDMTools. This document also demonstrated the process from a high level abstract VDM-SL model to a detailed VDM++ model taking more and more details into account.
• Dining Philosophers (Marcel Verhoef): This is the dining philosophers example. It is a classical example in the area of modelling concurrent systems.
• The Railway KLV example (Niels Kirkegaard): The main purpose of the KLV (Control Limitation Vitesse) on-board system is to provide a continuous train speed monitoring function. The origin of the simplied requirements come from Thierry Lecomte from Steria. The maximum allowed speed is obtained from the maximum train speed (which is a constant), from the topology of the track (declivity) and from the temporary speed restriction beacons. If the train speed does not comply with speed limits, emergency breaking is triggered.
• Specification of the SAFER system (Sten Agerholm): This specification is a VDM++ model of the SAFER (Simplified Aid for EVA Rescue) example presented in the second volume of the NASA guidebook on formal methods. Here Appendix C contains a complete listing of the SAFER system using PVS. We have translated this PVS specification rather directly into VDM-SL previously and here that model is again moved to VDM++. In the VDM++ model we have abstracted away form a number of parts which has been left as uninterpreted functions in the PVS model. This has been done because we have defined the purpose of the model to clarify the functionality of the thruster selection logic and the protocol for the automatic attitude hold functionality. Otherwise we have on purpose varied as little as possible from the given PVS model. In order to visualise this example the dynamic link feature is illustrated as well. More explanation about this work can be found in the papers:
  • Sten Agerholm and Peter Gorm Larsen, Modeling and Validating SAFER in VDM-SL, ed: Michael Holloway, in "Fourth NASA Langley Formal Methods Workshop", NASA, September 1997.
  • Sten Agerholm and Wendy Schafer, Analyzing SAFER using UML and VDM++, ed: John Fitzgerald and Peter Gorm Larsen, in "VDM Workshop at the Formal Methods 1999 conference, Toulouse
• Specification of a web server: This is a very simple VDM++ of the basic functionality of a web server.
• Basic Inheritence for Quadilaterals (Stephen Goldsack): This example deals with quadilaterals (figures with four straight lines) and the inheritence between them. A few basic operations are defined in the respective classes. This package also illustrates how to make use of C++ code automatically generated using VDMTools.
• Specification of the World Cup in Soccer: This example illustrates how one can define the rules for calculating who will qualify in the world championship in soccer given different initial groups. This model is made for the championship in 2000 but it could easily be updated to reflect the any championships.
• Specification of basic tree traversals and queues: This VDM++ model contains basic classes for defining and traversing over abstract threes and queues.
• Specification of a nuclear tracker (John Fitzgerald): This VDM++ model is a direct transformation from the VDM-SL model presented in the Fitzgerald&Larsen98 book on VDM-SL. The tracker takes care of monitoring and controlling the neclear material in a plant that takes care of processing such waste material.
• A railway interlocking system (Peter Gorm Larsen): This example is due to work carried out by Natsuki Terada from RTRI which has been translated from VDM-SL to VDM++. Thus there is limited use of inheritence but focus on a domain model for operational railways and in particular the requirements for a railway interlocking system ensuring that trains do not collide.
• A counter measures system for the aviodance of missiles (Peter Gorm Larsen and Marcel Verhoef): This example is used in the guidelines for developing distributed real time systems using the VICE extension to VDM++. This model is available in a sequential version , a concurrent version as well as in a distributed real-time VICE version . Each of these models are simply given at a more detailed granularity and before these a basic VDM-SL model was also made. That can be found in the VDM-SL examples repository.
• A Personal Medical Unit System (PMU) (Kasper H.J. Nielsen, Martin Kjelsen and Lars Sarbæk Kristiansen): A concurrent and a realtime VDM++ model of a real-time medico system: This project was completed at The Engineering College of Aarhus as a part of the course ”Model-driven development with VDM++ and UML 2” (tivdm2), with emphasis on concurrent and real-time development in VDMTools VICE toolbox.
• Verifiable File System: This is a Specification of the File System Layer, sliced at the FS_DeleteFileDir operation, as defined in the INTEL Flash File System document. It includes: a VDM++ model that can be model checked in an equivalent Alloy model; and an adapted version of the VDM++ model to be used in the Overture Automated Proof Support system.
• Master Thesis from the Engineering College of Aarhus, Denmark - Cand. Polyt. (Jasper Moltke Nygaard, Rasmus Ask Sørensen), "Evaluating Distributed Architectures using VDM++ Real-Time Modeling with a Proof of Concept Implementation", 7th. December 2007. This thesis will investigate and analyze the possibility of obtaining early stage validation of potential candidate system architectures, by means of formal modelling and validation. The goal is to analyze recent research extensions of VDM++ for describing and analyzing such distributed systems (VICE) and see if the language is suitable to stress test a distributed system and validate any architectural benets. Additionally this thesis will discus favorable approaches for realizing a case study of a transportation system in Tokyo, referred to as CyberRail. Different VDM++ models of candidate architectures for the CyberRail system has been developed and validated. This thesis includes 2 Real-Time VDM++ models (Backend Responsibility source, Joint Responsibility source), based on 2 different architectures. One of the architectures is realized as a prototype implementation in Java (source). Additionally a first draft of a distributed logging framework JAVTU (source), resembling the VDMTools interpreter execution trace log has been developed and a deployment manipulation tool Repeater (source) for setting up the deployment and the enviroment in VDMTools.

-- JasperNygaard - 13 Aug 2008