Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

AbstractPacemaker

This model is described in VDM-SL as a short, flat specification. 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_SL - vdm10
Details… model (zip) / show specification

AccountSys

This example comes from the book “Formal Software Development: From VDM to Java” written by Quentin Charatan and Aaron Kans. This example illustrate how to model bank accounts and transactions made on these as a series of deposits and withdrawals.

   
Author: Quentin Charatan and Aaron Kans
Version: VDM_SL - vdm10
Details… model (zip) / show specification

ACS

This specification describes the safety requirements involved in adding and removing explosives at an explosives storage site. The specification is based on United Kingdom Ministry of Defence regulations concerning safe storage of explosives, which in turn are based on UN regulations. Details of the specification may be found in:

  1. P. Mukherjee and V. Stavridou, “The Formal Specification of Safety Requirements for the Storage of Explosives”, technical report DITC 185/91, National Physical Laboratory, 1991.
  2. P. Mukherjee and V. Stavridou, “The Formal Specification of Safety Requirements for Storing Explosives”, Formal Aspects of Computing, 5(4):299-336, 1993. This example is primarily specified using the implicit style in VDM so it does not have a main debug functionality.
   
Author: Paul Mukherjee
Version: VDM_SL - vdm10
Details… model (zip) / show specification

ADT

This work specifies a number of abstract data types (ADT) in VDM-SL. This includes single-linked lists, double-linked lists, queues, stacks and binary trees. In addition this work is initiating a translation from VDM-SL to Modula-2 so system addressing and dynamic memory handing is specified in VDM-SL. This work was done by Matthew Suderman when he was a student at Trinity Western University in the Spring Semester, 1997.

   
Author: Matthew Suderman
Version: VDM_SL - classic
Details… model (zip) / show specification

AlarmErr

This is an erroneous version of the alarm example from the VDM-SL book, John Fitzgerald and Peter Gorm Larsen, Modelling Systems – Practical Tools and Techniques in Software Development}, Cambridge University Press, 2nd edition 2009. 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++.

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

Alarm

This is the alarm example from the VDM-SL book, John Fitzgerald and Peter Gorm Larsen, Modelling Systems – Practical Tools and Techniques in Software Development}, Cambridge University Press, 2nd edition

  1. 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++.
   
Author: John Fitzgerald and Peter Gorm Larsen
Version: VDM_SL - vdm10
Details… model (zip) / show specification

ATC

This example was developed by Natsuki Terada from the Japanese Railways Research Institute (RTRI) on a two year visit to IFAD in 2000 and 2001. It models a database for digital Automatic Train Control in Japan. More information can be found in:

Natsuki Terada, Formal Integrity Analysis of Digital ATC Database, In Proceedings of WCRR2001 (World Congress on Railway Research), 2001.

Natsuki Terada, Integrity Analysis of Digital ATC Database with Automatic Proofs, In VDM Workshop 3, Part of the FME 2002 conference, Copenhagen, Denmark, July 2002.

Natsuki Terada, Application of Formal Methods to Automatic Train Control Systems, In Proceedings of Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003), 2003.

N. Terada and M. Fukuda, Application of Formal Methods to the Railway Signaling Systems, In Quarterly Report of RTRI, 2002, Vol 43, no 4, pp 169-174.

   
Author: Natsuki Terada
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Bar

This specification was produced during a VDM-SL course presented by Peter Gorm Larsen to ICL Enterprise Engineering in 1994. The modelling of bags was one of the exercises the attendees (including the author Kevin Blackburn) was confronted with during the course. This specification is mainly intended for the purpose of illustrating how bags can be used. This is modelled using an executable subset and a collection of small tests are included.

   
Author: Kevin Blackburn
Version: VDM_SL - classic
Details… model (zip) / show specification

BOM

This specification was produced for VDM-SL courses presented by Peter Gorm Larsen in 1996. The modelling of a Bill Of Material (BOM) is a rather standard example making use of an Directed Acyclic Graph (DAG) structure.

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

Cashdispenser

This model is described in VDM-SL as a very abstract specification of how a pacemaker can pace a heart that is not having periodic stroken in the two heart chambers.

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

CM

The counter measures example was developed by Peter Gorm Larsen and Marcel Verhoef in 2007 in different dialect of VDM. This one is the most abstract version using VDM-SL.

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

ConwayGameLife

Conway’s Game of Life The universe of the Game of Life is an infinite two-dimensional orthogonal grid of square cells, each of which is in one of two possible states, alive or dead. Every cell interacts with its eight neighbours, which are the cells that are horizontally, vertically, or diagonally adjacent. At each step in time, the following transitions occur:

The initial pattern constitutes the seed of the system. The first generation is created by applying the above rules simultaneously to every cell in the seed-births and deaths occur simultaneously, and the discrete moment at which this happens is sometimes called a tick (in other words, each generation is a pure function of the preceding one). The rules continue to be applied repeatedly to create further generations.

   
Author: Nick Battle, Peter Gorm Larsen and Claus Ballegaard Nielsen (animation)
Version: VDM_SL - vdm10
Details… model (zip) / show specification

CountryColouring

This model has been translated by Peter Gorm Larsen from a similar model made in the RAISE Specification Language by Anne Haxthausen. It specifies relationships between countries on a map where naboring countries shall be coloured differently.

   
Author: Anne Haxthausen
Version: VDM_SL - classic
Details… model (zip) / show specification

Crossword

 This tutorial example is taken out of a VDM course given to the students of the Diplôme d’Etudes Supérieures Spécialisées en Génie Informatique (5th year) at the Université Joseph Fourier. This example uses the implicit style of specification of VDM-SL and thus may not be executed with the Overture debugger.

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

DepartureTMI

This is a model of an Air Traffic Flow Management (ATFM) departure Traffic Management Initiative (TMI) with the constraints:

Within these constraints, the goal is to allocate a take off time and runway to flights in an optimal manner. This model is making use of some of the newer language features such as set1.

   
Author: Paul Chisholm
Version: VDM_SL - vdm10
Details… model (zip) / show specification

DFDexample

This specification describes how one can automatically transform Data Flow Diagrams (DFD) into VDM-SL definitions. It is written as a flat VDM-SL model in a purely executable style. However, in order to test it at the top level one needs to construct a large test structure which essentially is an AST for a DFD. This have been done in the past but unfortunately the sources for this have been lost. This model was basis for a paper published as:

“A Formal Semantics of Data Flows Diagrams”, P.G.Larsen, N.Plat, H.Toetenel, Formal Aspects of Computing’’ 1994, Vol 6, December

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

Digraph

The specification describes how directed graphs and relations over such graphs can can tested for relevant properties and manipulated in different ways. This specification is produced by Janusz Laski from Oakland University in the USA. Most of the definitions in this specification can be interpreted.

This model is only an illustration of the problems germane to automatic software analysis. To get a better understanding of the scope of the analysis consult the text “Software Verification and Analysis, An Integrated, Hands-on – Approach,” by Janusz Laski w/William Stanley, Springer 2009. A brief online introduction is offered on the Website www.stadtools.com.

   
Author: Janusz Laski
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Dwarf

This is a VDM-SL Specification of the Dwarf Signal Controller. The VDM model made in this document is inspired by the Dwarf Signal control system described by Marcus Montigel, Alcatel Austria AG. The model is not complete in the sense that it does only model the handing of error situations for lamp L2. This have been presented at a FM Railway workshop by Peter Gorm Larsen and it has in the past been connected to a GUI using the VDMTools CORBA based API. Thus it is a fully executable specification.

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

Engine

As with many modern engineered products, the control software developed at Rolls- Royce is part of a larger system, namely an engine control system, comprising many electronic, hydromechanical and electromechanical components. The control system is part of an engine which, in turn, is a component of an aircraft. This VDM model is made by Greg Holland as a part of his MSc thesis in this area. It is made implicitly so it cannot be executed.

   
Author: Greg Holland
Version: VDM_SL - classic
Details… model (zip) / show specification

Express

The (building) industry in Europe currently uses the ISO-STEP standard to define information models with the aim to exchange data about those information models. The ISO-STEP standard contains the EXPRESS modelling language and several programming language bindings and an ASCII neutral format to implement interfaces to those models. Unfortunately, industry has not reached consensus on a particular information model, therefore multiple models exist. This raises the need to migrate instances from one model to another and vice-versa, commonly referred to as the “mapping”. The aim of this exercise was to determine the applicability of VDM-SL with respect to these types of problems. For more details on the mapping issue down- loadable copies of two papers resulting from this research is available. The example shows a simple VDM-SL abstract syntax representation of the ISO STEP part 21 physical file format and a transformation process for a particular set of abstract syntax instances. It implements a mapping between the relational model representation (rmrep) into a simple polynomial representation.

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

Gateway

This example is for a trusted gateway made by John Fitzgerald and Peter Gorm Larsen inspired by a more comprehensive model developed by British Aerospace. THe work undertaken here was published in:

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

Graph-ed

Alagar, Muthiayen and Periyasamy have developed formal specifications for a Graph Editor using VDM-SL. More information can be found in:

V.S. Alagar, D. Muthiayen and K. Periyasamy, “VDM-SL Specification of a Graph Editor”, Technical Report, Department of Computer Science, Concordia University, Montreal, Canada, May 1996.

   
Author: V. S. Alagar and D. Muthiayen and K. Periyasamy
Version: VDM_SL - vdm10
Details… model (zip) / show specification

HASL

This is a VDM-SL 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_SL - classic
Details… model (zip) / show specification

Hotel

This example is used to illustrate the difference between different formal approaches in the Alloy book. The example models a scheme for recodable hotel-door locks. More information can be found in:

Daniel Jackson, Software Abstractions, MIT Press, April 2006 ISBN 0-262-10114-9.

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

ISO8601

This is a model of dates, times and durations from the ISO8601 standard. It is intended as a core library for use by higher level models that require dates and/or times and/or durations. Dates are based on the Gregorian calendar. The Gregorian calendar commenced in October 1582, but it is extended backwards to year 1 in the proleptic Gregorian calendar, as per ISO 8601. Times assume Co-ordinated Univeral Time (UTC). Timezones and daylight savings are not supported. The granularity of times is to the nearest millisecond. A duration is modelled as a number of elapsed milliseconds (being the smallest unit of time). All functions are explicit and executable. Where a non-executable condition adds value, it is included as a comment.

   
Author: Paul Chisholm
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Library

This specification is for a bibliography database. It has been written by Anne Maarsel when she was a student working at OECD Halden Reator Project in the Summer of 1998. Note that this specification can be improved in various ways. First of all it introduces post-conditions that are not really adding much value since they are virtually identical to the explicit bodies. In addition the use of an optional type instead of would be appropriate here.

   
Author: Anne Maarsel
Version: VDM_SL - classic
Details… model (zip) / show specification

Loose

This VDM model is made by Peter Gorm Larsen as an exploration of how the looseness in a subset of VDM-SL. So this is illustrating how it is possible to explore all models is a simple fashion including the possibility of recursive functions where looseness is involved inside each recursive call. A paper about this work have been published as:

Peter Gorm Larsen, Evaluation of Underdetermined Explicit Expressions, Formal Methods Europe’94: Industrial Benefit of Formal Methods, Springer Verlag, October 1994.

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

LUHN

Luhn algorithm See http://en.wikipedia.org/wiki/Luhn_algorithm

The Luhn algorithm or Luhn formula, also known as the “modulus 10” or “mod 10” algorithm, is a simple checksum formula used to validate a variety of identification numbers, such as credit card numbers, IMEI numbers, National Provider Identifier numbers in US and Canadian Social Insurance Numbers. It was created by IBM scientist Hans Peter Luhn and described in U.S. Patent No. 2,950,048, filed on January 6, 1954, and granted on August 23, 1960.

The algorithm is in the public domain and is in wide use today. It is specified in ISO/IEC 7812-1.[1] It is not intended to be a cryptographically secure hash function; it was designed to protect against accidental errors, not malicious attacks. Most credit cards and many government identification numbers use the algorithm as a simple method of distinguishing valid numbers from collections of random digits.

   
Author: Nick Battle
Version: VDM_SL - vdm10
Details… model (zip) / show specification

LUP

This VDM model is made by Lothar Schmitz and it has taken different standard algorithms for the length of longest upsequence problem from David Gries and Janusz Laski (see references below). Different versions of the algorithms are included. See also:

David Gries: The Science of Programming, Springer-Verlag 1981, pp. 259-262.

Janusz Laski und William Stanley, Software Verification and Analysis, Springer-Verlag, 2009.

   
Author: Lothar Schmitz
Version: VDM_SL - vdm10
Details… model (zip) / show specification

MAA

This specification is of the Message Authenticator Algorithm (MAA) standard is used in the area of data security in banking and the scope of the standard is authentication. More details can be found in:

G.I. Parkin and G O’Neill, “Specification of the MAA standard in VDM’’, In S. Prehn and W.J. Toetenel (eds), “VDM’91: Formal Software Development Methods’’, Springer-Verlag, October 1991.

   
Author: Graeme Parkin
Version: VDM_SL - classic
Details… model (zip) / show specification

Metro

This model presents three different abstract specifications of a metro door management system in VDM-SL. The purpose of the presentation is to describe alternatives to the Metro specification developed in the European research project called SPECTRUM.

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

Monitor

This example comes from the VDM-SL book by John Fitzgerald and Peter Gorm Larsen. It is the running example through the chapter about logic. Suppose we are asked to develop the software for a temperature monitor for a reactor vessel in the plant. The monitor is connected to a temperature sensor inside the vessel from which it receives a reading(in degrees Celsius) every minute.

The monitor records the five most recent temperature readings in the order in which they were received from the sensor.

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

NDB

The Non-programmer database system (NDB) is a nicely engineered binary relational database system invented by Norman Winterbottom of IBM. The formal Specification of NDB was originally undertaken by Anne Walshe, who has subsequently documented the specification and its refinement. NDB has been used as an example problem for modular specification in VDM-SL. However, the version available here is a “flat” specification. The postscript file includes a significant description of the validation of the specification using execution. Test coverage is not used though. Relevant publications are:

A. Walshe, “NDB: The Formal Specification and Rigorous Design of a Single-User Database System”, in C.B. Jones and R.C. Shaw (eds), “Case Studies in Systematic Software Development”, Prentice Hall 1990, ISBN 0-13-116088-5

J.S. Fitzgerald and C.B. Jones, “Modularizing the Formal Description of a Database System”, in D. Bjorner, C.A.R. Hoare and H. Langmaack (eds), VDM ‘90: VDM and Z - Formal Methods in Software Development, Springer-Verlag, LNCS 428, 1990

   
Author: Rich Bradford
Version: VDM_SL - classic
Details… model (zip) / show specification

Newspeak

The programming language NewSpeak? is a language designed specifically for use in safety-critical systems. It employs the notion of Orwellian programming - undesirable properties are avoided by restricting the syntax of the programming language. This is a formal semantics for the language in VDM-SL. Details of the language and its semantics:

P. Mukherjee, “A Semantics for NewSpeak? in VDM-SL”. In T. Denvir, M. Naftalin, M. Bertran (eds), “FME ‘94: Industrial Benefit of Formal Methods”, Springer-Verlag, October 1994.

I.F. Currie, “NewSpeak - a reliable programming language”. In C. Sennett (ed), “High-Integrity Software”, Pitman 1989.

   
Author: Paul Mukherjee
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Pacemaker

The Pacemaker Challenge problem has been proposed by the North American Software Certification Consortium, based on a pacemaker specification offered by Boston Scientific. Participants in the challenge are invited to develop models, designs and implementations, as well as generating evidence that would be of value in certifying the software. More details can be found in:

Hugo Daniel Macedo, Peter Gorm Larsen and John Fitzgerald, Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM, FM 2008: Formal Methods, LNCS 5014, Eds.: Jorge Cuellar, Tom Maibaum and Kaisa Sere, May 2008.

   
Author: Hugo Macedo
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Planner

The specification is of the input language, and the central operations, of a domain-independent, partial order, constraint posting goal directed planner. It is essentially a model-based version of Chapman’s TWEAK (1), and is used as a case study on VDM courses at the Univ. of Huddersfield. It is described fully, and prototyped in Prolog, in (2).

Planning for Conjunctive Goals, D.Chapman, AI Journal no 32, 1987.

The Construction of Formal Specifications: an Introduction to the Model-Based and Algebraic Approaches, J.Turner and McCluskey, McGraw-Hill Software Engineering Series, London. ISBN 0-07-707735-0.

   
Author: T.L. McCluskey and Pat Diskin
Version: VDM_SL - classic
Details… model (zip) / show specification

ProgLang

This example is made by Bernhard K. Aichernig and Andreas Kerschbaumer and it contains a VDM model for a Static and Dynamic Semantics of a Simple Programming Language. The example has been an assignment in the exercises of the software technology course at the Technical University Graz, Austria.

   
Author: Bernhard K. Aichernig and Andreas Kerschbaumer
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Raildir

In this specification a model of interlocking systems is presented, and it is describe how the model may be validated by simulation. Station topologies are modelled by graphs in which the nodes denote track segments, and the edges denote connectivity for train traffic. Points and signals are modelled by annotations on the edges, thereby restricting the driving possibilities. We define the safe station states as predicates on the graph, and present a first step towards an implementation of these predicates. The model development illustrates how concepts may be captured and validated for a non-trivial system. This work was conducted by Kirsten Mark Hansen work for the Danish State Railways. More about this work can be found at:

K.M. Hansen, Formalising Railway Interlocking Systems, Nordic Seminar on Dependable Computing Systems, Department of Computer Science, Technical University of Denmark, August 1994, pp. 83-94.

Kirsten Mark Hansen. Linking Safety Analysis to Safety Requirements

   
Author: Kirsten Mark Hansen
Version: VDM_SL - classic
Details… model (zip) / show specification

Realm

This document is simply an attempt to model the basic data structures and auxiliary functions necessary to represent realms. A geometric realm defined here is a planner graph over a finite resolution grid. This example have been partly tested and the test coverage information is displayed on the postscript version of the document. The script used for testing is included among the source files. Realms are used to represent geographical data. This document is based on:

Realms: A Foundation for Spatial Data Types in Database Systems, Ralf Hartmut Güting and Marcus Schneider, Advances in Spatial Databases - Third International Symposium, SSD’93, Springer-Verlag, June 1993.

Map Generalisation, Ngo Quoc Tao, UNU/IIST, Macau, Draft, January, 1996.

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

Recursive

This example is made by John Fitgerald and Peter Gorm Larsen and it is used in the chapter about recursion in the second edition of the VDM-SL book. It contains a number of examples for recursive graph structures and functionality over such graphs.

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

SAFER

This VDM-SL model is a response to the PVS model of the SAFER system for NASA austronauts used for space walks used to maneuver back to a space shuttle. It was made by Sten Agerholm and Peter Gorm Larsen and published as:

S.Agerholm and P.G.Larsen, Modeling and Validating SAFER in VDM-SL, Proceedings of the Fourth NASA Langley Formal Methods Workshop, NASA Conference, Publication 3356, September 1997.

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

Shmem

This example was produced by Nick Battle and it is used in the VDMJ user manual to illustrate different features of VDMJ. It models the behaviour of the 32-bit shared memory quadrants of HP-UX, using a record type M to represent a block of memory which is either or , and a sequence of M records to represent a Quadrant.

The specification output indicates which allocation policy, first-fit or best-fit (or neither), produces the most memory fragmentation.

   
Author: Nick Battle
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Simulator

The simulator specified in VDM-SL in this example is the main component of an animation tool designed for use in the validation of complex real-time reactive systems described using TROM (Timed Reactive Object Model) formalism. We include two versions of the specifications; Section 2 contains the version in which implicit operations are used, and most of the operations are rewritten as explicit operations in the version contained in Section 3.

   
Author: V. S. Alagar \and D. Muthiayen
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Soccer

This tutorial example is taken out of a VDM course given to the students of the Diplôme d’Etudes Supérieures Spécialisées en Génie Informatique (5th year) at the Université Joseph Fourier. A first version uses the implicit style of specification of VDM-SL and thus may not be executed with VDMTools. An explicit version is given as an appendix.

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

STV

This model aims to model a single transferable voting system used for electronic voting. It is further described in the following papers:

P. Mukherjee and B.A. Wichmann. Formal Specification of the STV Algorithm. In M.G. Hinchey and J. P. Bowen, editors, Applications of Formal Methods. Prentice Hall, 1995.

Paul Mukherjee, Automatic translation of VDM-SL specifications into gofer, Springer, Lecture Notes in Computer Science, Volume Volume 1313/1997 Book FME ‘97: Industrial Applications and Strengthened Foundations of Formal Methods

   
Author: Paul Mukherjee
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Telephone

This example due to Abrial has been translated from the B-notation into VDM-SL. It demonstrates how an event-based system may be modeled using the specification language of the Vienna Development Method. In the following, operations specify the events which can be initiated either by the system or by a subscriber (user). An implicit style using pre- and post-conditions has been chosen, in order to model the system’s state transitions. The model of the telephone exchange is centred around a set of subscribers who may be engaged in telephone conversations through a network controlled by an exchange.

   
Author: Bernhard Aichernig
Version: VDM_SL - classic
Details… model (zip) / show specification

Tic-tac-toe

A standard Tic-tac-toe game

   
Author: Nick Battle
Version: VDM_SL - vdm10
Details… model (zip) / show specification

Tracker

The tracker example is used in the mapping chapter of the VDM-SL book by John Fitzgerald and Peter Gorm Larsen to introduce mappings and mapping operators concerns a system for tracking the movement of containers of hazardous material between phases of processing in a nuclear reprocessing plant. It is inspired by the formal model of a plant controller architecture developed by Manchester Informatics Ltd. in collaboration with British Nuclear Fuels (Engineering) Ltd. (BNFL) in 1995. More can be read about this in:

J.S. Fitzgerald and C.B. Jones, Proof in VDM: Case Studies, Chapter: Proof in the Validation of a Formal Model of a Tracking System for a Nuclear Plant, Springer-Verlag, FACIT Series, 1998.

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

Traffic

This example is for all small traffic light control kernel presented in the VDM-SL book of John Fitzgerald and Peter Gorm Larsen. It was originally inspired by a similar model made in Z by Paul Ammann. A paper about this written long ago:

A safety kernel for traffic light control, Paul Ammann, Aerospace and Electronic Systems Magazine, IEEE, February 1996, Volume: 11 Issue: 2, pp. 13 - 19, ISSN: 0885-8985.

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

VCParser-master

This example is created by Tomohiro Oda and it illustrates how it is possible to use higher-order functions in VDM-SL to create parser elements that can be put together in a compositional fashion. This model can be used as a kind of library that one can play with manipulating strings into a VDM AST representation.

   
Author: Tomohiro Oda
Version: VDM_SL - vdm10
Details… model (zip) / show specification