Overture Tool

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.

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.

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.

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.

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++.

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++.

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.

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.

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.

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.

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.

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:

• Any live cell with fewer than two live neighbours dies, as if caused by under-population.
• Any live cell with two or three live neighbours lives on to the next generation.
• Any live cell with more than three live neighbours dies, as if by overcrowding.
• Any dead cell with exactly three live neighbours becomes a live cell, as if by reproduction.

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.

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.

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.

DepartureTMI

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

• a set of flights wish to depart an airport;
• each flight may only take off from certain runways;
• each flight has a preferred take off time;
• each flight has an acceptable take off window;
• only certain runways are available;
• runways have a maximum rate at which departures can take place;
• the TMI runs for a specific time interval.

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.

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

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.

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.

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.

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.

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:

• Peter Gorm Larsen, Tom Brookes, Mike Green and John Fitzgerald, A Comparison of the Conventional and Formal Design of a Secure System Component, Nordic Seminar on Dependable Computing Systems, August, 1994.

• J.S. Fitzgerald, T.M. Brookes, M.A. Green, and P.G. Larsen, Formal and Informal Specifications of a Secure System Component: first results in a comparative study, Formal Methods Europe’94 - : Industrial Benefit of Formal Methods, Springer Verlag, October 1994.

• Peter Gorm Larsen, John Fitzgerald, Tom Brookes, Mike Green, Formal Modelling and Simulation in the Development of a Security-critical Message Processing System, Anglo-French workshop on Formal Methods, Modelling and Simulation for System Engineering, Saint-Quentin, France, February, 1995.

• John Fitzgerald, Peter Gorm Larsen, Tom Brookes and Mike Green, Developing a Security-critical System using Formal and Conventional Methods, Chapter 14 in “Applications of Formal Methods”, M.G. Hinchey and J.P. Bowen (editors), Prentice Hall International Series in Computer Science, September 1995.

• Peter Gorm Larsen, John Fitzgerald and Tom Brookes, Lessons Learned from Applying Formal Specification in Industry, IEEE Software, pp 48-56, May 1996.

• T.M. Brookes, J.S. Fitzgerald, and P.G. Larsen, Formal and Informal Specifications of a Secure System Component: final results in a comparative study, “Formal Methods Europe’96”, pp 214-227, Springer Verlag, March 1996.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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

• Exemplified by Railway Interlocking Systems. PhD thesis, Department of Information Technology, Technical University of Denmark, 1996.

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.

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.

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.

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.

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.

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.

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

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.

Tic-tac-toe

A standard Tic-tac-toe game

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.

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.

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.

Xml

This example is a simple AST for XML and utilities to manipulate it. This model is originally intended to construct SVG models to specify GUIs for interactive systems.