Overture Tool

CarNaviRadio

The origin of the car radio navigation example comes from Marcel Verhoef as a part of his PhD thesis where it was used to compary different formalisms. This example shows how an embedded application with both radio, navigation and traffic messages are joined in one coherent application in a distributed application.

CarNaviRadioValConj

This example is a modified version of the car radio navigation example. It demonstrates the use of validation conjectures.

The origin of the car radio navigation example comes from Marcel Verhoef as a part of his PhD thesis where it was used to compare different formalisms. This example shows how an embedded application with both radio, navigation and traffic messages are joined in one coherent application in a distributed application.

ChessWay

This example shows the discrete event model used for co-simulation of the ChessWay personal people mover as used in the DESTECS project (see http://www.destecs.org). It reflects the status of the model which is mentioned in the paper A Formal Approach to Collaborative Modelling and Co-simulation for Embedded Systems which is submitted to the Journal Mathematical Structures in Computer Science. The corresponding continuous time model is available through the first author.

CM

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. This is the distributed real time version of this example.

CyberRail

This VDM-RT model was produced as a part of an MSn thesis investigating and analyzing the possibility of obtaining early stage validation of potential candidate system architectures, by means of formal modelling and validation. The goal was to analyze recent research extensions of VDM++ for describing and analyzing such distributed systems (VDM-RT) and see if the language is suitable to stress test a distributed system and validate any architectural benefits. Additionally this thesis discusses 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.

HomeAutomation

This is a distributed real-time version of a home automation example constructed by Sune Wolff.

More information can be found in: Peter Gorm Larsen, John Fitzgerald and Sune Wolff, Methods for the Development of Distributed Real-Time Embedded Systems Using VDM, International Journal of Software and Informatics, Vol 3., No 2-3, June/September 2009, pp. 305-341.

Iioss

This project was made by Christian Thillemann and Bardur Joensen in a VDM course. It is modelling a small subset of a controller for a pig stable that wish to keep track of the whereabouts of a collection of pigs in a stable.

MSAW

This example is created by Augusto Ribeiro illustrating different concepts in VDM for teaching purposes including the distributed real time features in VDM-RT. Note that thus this model is not in a state where it makes sense to execute it.

Oldcarradio

This was the first model Marcel Verhoef tried to make of the car radio navigation example using the original version of VICE with one CPU. This failed and as a consequence Marcel Verhoef and Peter Gorm Larsen came up with an improved version of VDM-RT with multiple CPUs connected with BUSses.

Pacemaker

This model is made by Hugo Macedo as a part of his MSc thesis of a pacemaker according to the grand challenge provided by Boston Scientific in this area. This is the last of a series of VDM models of the pacemaker and it incorporates a number of modes for the pacemaker. More information can be found in:

Hugo Macedo, Validating and Understanding Boston Scientific Pacemaker Requirements, MSc thesis, Minho University, Portugal, October 2007.

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 FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Eds, Jorge Cuellar and Tom Maibaum and Kaisa Sere, 2008, Springer-Verlag, Lecture Notes in Computer Science 5014, pp. 181–197.

Robot

This example was produced by Lasse Lorentzen and Kenneth Lausdahl as a part of a VDM course of a robot travelling autonomically inside a cave aiming at avioding different obstacles on its path.

VDM

VeMo

This example was used in the MSc thesis for Claus Ballegaard Nielsen in order to illustrate how dynamic deployment with advantage could be added to VDM-RT.

More information can be found in: Nielsen, C.B.: Dynamic Reconfiguration of Distributed Systems in VDM-RT. Master’s thesis, Aarhus University (December 2010).