Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Access-control

This specification describes access control and policies for restricting this. Details of the specification may be found in:

  1. Formal Engineering of Access Control Policies in VDM++ Jeremy W. Bryans and John S. Fitzgerald. In proceedings of 9th International Conference on Formal Engineering Methods (ICFEM 2007). Boca Raton, USA, November 2007. pp 37–56

  2. A Formal Approach to Dependable Evolution of Access Control Policies in Dynamic Collaborations Jeremy W. Bryans, John S. Fitzgerald and Panos Periorellis. In Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, pp 352-353, Supplemental Volume. June 25-28, 2007. Edinburgh, UK

   
Author: Jeremy Bryans and John Fitzgerald
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Alarm++proof

This is a version of the alarm example from the VDM++ book, John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef, Validated Designs for Object-oriented Systems, Springer, New York. 2005, ISBN 1-85233-881-4. This version of the example has been used for proof purposes and thus the operations in the normal VDM++ of this example are made as functions just like in the VDM-SL version of the alarm example. The example is inspired by a subcomponent of a large alarm system developed by IFAD A/S. It is modelling the management of alarms for an industrial plant. The purpose of the model is to clarify the rules governing the duty roster and calling out of experts to deal with alarms.

   
Author: John Fitzgerald and Peter Gorm Larsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Alarm++traces

This is a version of the alarm example from the VDM++ book where traces have been added to test automation purposes. See John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef, Validated Designs for Object-oriented Systems, Springer, New York. 2005, ISBN 1-85233-881-4. The example is inspired by a subcomponent of a large alarm system developed by IFAD A/S. It is modelling the management of alarms for an industrial plant. The purpose of the model is to clarify the rules governing the duty roster and calling out of experts to deal with alarms. A comparable model of this example also exists in VDM-SL.

   
Author: John Fitzgerald and Peter Gorm Larsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

AlarmErr

This is an erronerous version of the alarm example from the VDM++ book, John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef. Validated Designs for Object-oriented Systems, Springer, New York. 2005, ISBN 1-85233-881-4. This version of the example is used for illustrating the tool support in tutorial material about Overture. It is inspired by a subcomponent of a large alarm system developed by IFAD A/S. It is modelling the management of alarms for an industrial plant. The purpose of the model is to clarify the rules governing the duty roster and calling out of experts to deal with alarms. A comparable model of this example also exists in VDM-SL.

   
Author: John Fitzgerald and Peter Gorm Larsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Alarm

This is the alarm example from the VDM++ book, John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef. Validated Designs for Object-oriented Systems, Springer, New York. 2005, ISBN 1-85233-881-4. The example is inspired by a subcomponent of a large alarm system developed by IFAD A/S. It is modelling the management of alarms for an industrial plant. The purpose of the model is to clarify the rules governing the duty roster and calling out of experts to deal with alarms. A comparable model of this example also exists in VDM-SL.

   
Author: John Fitzgerald and Peter Gorm Larsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

AutomatedStockBroker

The system is an automated stock broker, where you can specify a list of stocks which automaticly, can either be bought or sold. This is done by defining a prioritised list of stocks to observe, which each has defined a trigger that tells in which situation the system should react with either a buy or a sell action. The trigger is a rule defined upon the history and the current value of the stock. This model is made by Anders Kaels Malmos as a small mini-project in a course on “Modelling of Mission Critical Systems” (see https://services.brics.dk/java/courseadmin/TOMoMi/pages/Modelling+of+Mission+Critical+Systems).

More information about the model and the purpose of it can be found in the ProjectReport.pdf file included in the zip file with the source files.

   
Author: Anders Kaels Malmos
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Autopilot

   
Author:  
Version: VDM_PP - classic
Details… model (zip) / show specification

Buffers

This model is made by Yves Ledru et al. in a paper illustrating the combinatorial testing tool called Tobias. In this model the traces to be used for combinatorial testing purposes have been redone by Peter Gorm Larsen. For more information see:

Filtering TOBIAS Combinatorial Test Suites, Yves Ledru, Lydie du Bousquet, Olivier Maury and Pierre Bontron, In Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, Springer, ISSN 0302-9743 (Print) 1611-3349 (Online), Volume 2984/2004.

   
Author: Yves Ledru
Version: VDM_PP - classic
Details… model (zip) / show specification

Buslines

This example models bus lines in a city, in which passengers are to be transferred from stop to stop. Passengers with specific destinations will arrive at a central station, and the route and flow of the buses need to be planned to service the passenger in the best possible way. The number and routes of buses as wells as the inflow of passengers are variables.

Remote Debugger must be set to remote class: gui.BuslinesRemote

   
Author: Claus Ballegaard Nielsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

BuslinesWithDB

This example models bus lines in a city, in which passengers are to be transferred from stop to stop. Passengers with specific destinations will arrive at a central station, and the route and flow of the buses need to be planned to service the passenger in the best possible way. The number and routes of buses as wells as the inflow of passengers are variables.

This version connects to a database containing maps and busroutes.

Remote Debugger must be set to remote class: gui.BuslinesRemote

   
Author: Claus Ballegaard Nielsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

CashDispenserConc

This model is concurrent and it is described in VDM++. This enables abstraction from design considerations and can model errors in the communication channel and it ensures maximum focus on high-level, precise and systematic analysis. This was developed by Sten Agerholm, Peter Gorm Larsen and Kim Sunesen in 1999 in connection with FM’99.

   
Author: Sten Agerholm, Peter Gorm Larsen and Kim Sunesen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

CashDispenser

This model is described in the sequential subset of VDM++. This enables abstraction from design considerations and ensures maximum focus on high-level, precise and systematic analysis. This was developed by Sten Agerholm, Peter Gorm Larsen and Kim Sunesen in 1999 in connection with FM’99.

   
Author: Sten Agerholm, Peter Gorm Larsen and Kim Sunesen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

CMConc

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.

   
Author: Peter Gorm Larsen and Marcel Verhoef
Version: VDM_PP - vdm10
Details… model (zip) / show specification

CMSeq

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.

   
Author: Peter Gorm Larsen and Marcel Verhoef
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Codegen

This example is produced by a group of students as a part of a VDM course given at the Engineering College of Aarhus. This model describes how to do code generation from a small applicative language called Simple to a subset of Java (called Geraffe). This example also illustrates how one can make use of Java jar files as a part of a VDM model supported by Overture.

   
Author: Johannes Ulfkjær Jensen, Jon Nielsen and Leni Lausdahl
Version: VDM_PP - classic
Details… model (zip) / show specification

Concfactorial

This example is made by Nick Battle and it illustrates how one can perform the traditional factorial functionality using the concurrency primitives in VDM++.

   
Author: Nick Battle
Version: VDM_PP - classic
Details… model (zip) / show specification

Diet2japan

This example is made by Shin Sahara as a test of local higher order functions defined inside explicit function definitions in order to test the correct interpretation of these constructs.

   
Author: Shin Sahara
Version: VDM_PP - classic
Details… model (zip) / show specification

Dining

This example is made by Marcel Verhoef and it demonstrates the standard classical dining philosophers problem expressed in VDM++. The standard launcer provided here is sufficient to cover the entire VDM++ model.

   
Author: Marcel Verhoef
Version: VDM_PP - classic
Details… model (zip) / show specification

ElectronicPurse

This example is made by Steve Riddle as an example for an exam question used at the VDM course in Newcastle. It deals with an electronic purse in a simple form. This is one of the grand challenges that is considered by the formal methods community for formal verification.

   
Author: Steve Riddle
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Enigma

This VDM++ model is developed by Marcel Verhoef as a part of the VDM++ book John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef. Validated Designs for Object-oriented Systems, Springer, New York. 2005, ISBN 1-85233-881-4. This is a VDM++ model of the famous Enigma cipher machine used by the Germans in the Second World War to encrypt and decrypt messages that were exchanged between military units. The purpose of the model is to get a basic understanding of the cipher mechanism as implemented in Enigma. This example was the first place where the VDMUnit testing approach was introduced.

   
Author: Marvel Verhoef
Version: VDM_PP - vdm10
Details… model (zip) / show specification

HomeAutomationConc

   
Author:  
Version: VDM_PP - classic
Details… model (zip) / show specification

HomeautomationSeq

This is a sequential VDM++ 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.

   
Author: Sune Wolff
Version: VDM_PP - classic
Details… model (zip) / show specification

KLV

This example describes a VDM++ specification of a KLV system. The purpose of the KLV system is to provide a continuous monitoring of the speed of a train. The VDM++ specification is inspired by a KLV description provided to the EP26538 FMERail project as case study by Atelier B. This model shows an example of how an informal description can be translated into a precise model that together with a graphical front-end can be used to ensure that the customer and the developer have a common interpretation of the system under development.

The focus of the model is on the logic of the KLV systems when a train meets speed restriction beacons along the tracks, i.e. on events that triggers the KLV system. Issues such as how to determine whether a beacon has been met within a certain distance calculated from speed has been abstracted in away in the current model. They could be issues to extend the model with.

   
Author: Niels Kirkegaard
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Memoryproof

   
Author:  
Version: VDM_PP - classic
Details… model (zip) / show specification

MetroInterlocking

This example is produced by a student as a part of a VDM course given at the Department of Engineering at the University of Aarhus. This model describes a small interlocking system for a metro.

   
Author: Steffen Diswal
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Mondex

   
Author:  
Version: VDM_PP - classic
Details… model (zip) / show specification

MSAWconcur

This VDM++ model is made by August Ribeiro as input for the VDM courses delivered at IHA in Denmark. It is a concurrent version of the Minimum Safety Altitude Warning System (MSAW) example.

This project is currently not running with the Overture interpreter.

   
Author: Augusto Ribeiro
Version: VDM_PP - vdm10
Details… model (zip) / show specification

MSAWseq

This VDM++ model is made by August Ribeiro as input for the VDM courses delivered at IHA in Denmark. It is a concurrent version of the Minimum Safety Altitude Warning System (MSAW) example.

2011-12-28 This VDM++ model has been updated by Rasmus Lauritsen with the addition of a swing java radar display. The Radar.vdmpp model is now hooked up the with Radar display. The radar display will make a 360 degrees scan everytime the “Scan” operation on the Radar is invoked.

lib/radar.jar contains binary and source code for the java radar display.

   
Author: Augusto Ribeiro
Version: VDM_PP - vdm10
Details… model (zip) / show specification

PacemakerConc

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.

   
Author: Hugo Macedo
Version: VDM_PP - classic
Details… model (zip) / show specification

PacemakerSeq

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.

   
Author: Hugo Macedo
Version: VDM_PP - classic
Details… model (zip) / show specification

PacemakerSimple

This model is a very simple version of the pacemaker as it has been used for a small exercise to VDM newcommers. It was first used in a VDM course delivered by Steve Riddle and John Fitzgerald and later used and adjusted by Peter Gorm Larsen also.

   
Author: Steve Riddle and Peter Gorm Larsen
Version: VDM_PP - classic
Details… model (zip) / show specification

POP3

This example is written by Paul Mukherjee and it is used in the VDM++ book John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef. Validated Designs for Object-oriented Systems, Springer, New York. 2005, ISBN 1-85233-881-4. The concurrent system in question is a server for the POP3 protocol. This is a protocol supported by all major email c lients to fetch email messages from the email server.

   
Author: Paul Mukherjee
Version: VDM_PP - classic
Details… model (zip) / show specification

ProductLine

   
Author: Naoyasu Ubayashi, Shin Nakajima and Masayuki Hirayama
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Quadilateral

This example deals with quadilaterals (figures with four straight lines) and the inheritance 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.

   
Author: Stephen Goldsack
Version: VDM_PP - vdm10
Details… model (zip) / show specification

ReaderWriter

   
Author:  
Version: VDM_PP - vdm10
Details… model (zip) / show specification

SAFER

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. In the test class Test there are a few examples of using the traces primitives used for test automation.

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

   
Author: Sten Agerholm and Peter Gorm Larsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

SAFERProof

   
Author: Sten Agerholm
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Smoking

   
Author: Claus Ballegaard Nielsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

SortingParcels

The purpose of this VDM++ model is to analyse the rules governing for distributing parcels with different kinds of goods is a warehouse. This model is made by Bjarke Møholt as a small mini-project in a course on “Modelling of Mission Critical Systems” (see https://services.brics.dk/java/courseadmin/TOMoMi/pages/Modelling+of+Mission+Critical+Systems).

   
Author: Bjarke Møholt
Version: VDM_PP - vdm10
Details… model (zip) / show specification

SortPP

This VDM++ model is made by Peter Gorm Larsen in 2010 based on the original VDM++ model created many years ago at IFAD.

   
Author: Peter Gorm Larsen
Version: VDM_PP - vdm10
Details… model (zip) / show specification

SSlibE2

This example contains a large collection of test classes that can be used to test different aspects of VDM++. This makes use of the VDMUnit test approach.

   
Author: Shin Sahara
Version: VDM_PP - classic
Details… model (zip) / show specification

Stack

   
Author:  
Version: VDM_PP - vdm10
Details… model (zip) / show specification

TempoCollaborative

This is a brief description on how to run the TEMPO demonstrator, and how to configure it. This is without the graphical extensions made in the project for Overture: for the use of those we refer to the associated manuals. The below is still relevant if you want to use the graphical extensions, though.

The demonstrator is executed by launching a run configuration. So in order to do that you have to make one. A typical example has the following parameters:

The operation “Run” takes three parameters:

All configuration files are .csv, so basically comma seperated text files.

The following files are relevant:

** Network desscription **

This file contains the following information for every edge in the network:

An example line in the file could be: “A201”,”A20S”,”A20A4”,1,2,70,240

** TMS description **

This file contains the following information for every TMS in the network:

An example line in the file could be: “RWS”,”A152”,”HardShoulder”,1,nil

** Geographic description **

This is only relevant for the Java simulator. The file should always have the name “GeoInfo.csv”. It specifies the geographic location in terms of GPS coordinates for each node in the network, so that the simulator knows where to plot it on the map.

** Events **

Describes the events that take place during the simulation. Each line contains:

An example line in the file could be: 1220,”SetInputStream”,”A153”,5

** Use of Overture Graphics Support **

As a part of the TEMPO project a new plug-in on top of the Overture tool called the “Overture Graphics Plugin Development”. Thus, it is possible to update versions of Overture version 2.4.0 or higher under “Help -> Install New Software” inside the Overture Eclipse tool. After having installed the plug-in it is possible to add this feature for a specific project by selecting “Overture Graphics -> Add Overture Graphics Library” by right-clicking on a project. When this have been carried out debugging can be started with a special “Vdm Graphics Application” and this will start up a seperate Electron application called the “Overture Graphics Plugin”. Here one need to choose the root class (in this case “World”) and afterwards what top-level method to run (in this can one can either select “run” or “runwithoutcollab”). Afterwards, it is possible to define multiple plots which can be viewed while a VDM simulation is on-going (either in 2D or 3D). For this model it makes sense to monitor “tmsX.averagedensity” and “tmsX.averagevelocity” where X is either 1 or 2. Finally, it is possible to select a plot and dooble click on it and then start the VDM simulator with the selected operation. In this case a new GUI (programmed in Java) will come up and then from there the entire simulation can be started up.

   
Author:  
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Trackerproof

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 nuclear material in a plant that takes care of processing such waste material.

   
Author: John Fitzgerald
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Trayallocation

This VDM++ model is made by two students of a sortation system able to sort parcels into different trays for example for an airport sorting suitcases for different flights. The model here focus on the algorithm for prioritising between different feeders to the conveyer belt

   
Author: Kim Bjerge and José Antonio Esparza Jaesparza
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Tree

This VDM++ model contains basic classes for defining and traversing over abstract threes and queues.

   
Author:  
Version: VDM_PP - vdm10
Details… model (zip) / show specification

VFS

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. In the test class UseFileSystemLayerAlg there are a few examples of using the traces primitives used for test automation. This model has been developed by Miguel Ferreira

   
Author: Miguel Ferreira
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Webserver

This is a very simple VDM++ of the basic functionality of a web server.

   
Author:  
Version: VDM_PP - vdm10
Details… model (zip) / show specification

Worldcup

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. In the test class UseGP there are a few examples of using the traces primitives used for test automation.

   
Author: Yves Ledru
Version: VDM_PP - vdm10
Details… model (zip) / show specification