This page provides a series of substantial, freely available 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.
If you have access to the CSK VDMTools you can actually analyse the source texts further.
All 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.
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.
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.
This is the dining philosophers example. It is a classical example in the area of modelling concurrent systems.
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.
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. 1. 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.
This is a very simple VDM++ of the basic functioinality of a web server.
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.
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 next championship.
This VDM++ model contains basic classes for defining and traversing over abstract threes and queues.
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.
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.
Last update January 2006