- Vienna Development Method
The Vienna Development Method (VDM) is one of the longest-established
Formal Methods for the development of computer-based systems. Originating in work done at IBM's Vienna Laboratory [Some idea of that work, including a technical report TR 25.139 on "A Formal Definition of a PL/1 Subset, dated 20 December 1974, is given in Bekič&Jones 1984, p.107-155. Of particular note is the list of authors in order: H. Bekič, D. Bjørner, W Henhapl, C. B. Jones, P. Lucas.] in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language - the VDM Specification Language (VDM-SL). It has an extended form, VDM++ [The double plus is adopted from the [http://en.wikipedia.org/wiki/C%2B%2B C++] objected oriented programming language based on C.] , which supports the modeling ofobject-oriented and concurrent systems. Support for VDM includes commercial and academic tools for analyzing models, including support for testing and proving properties of models and generating program code from validated VDM models. There is a history of industrial usage of VDM and its tools and a growing body of research in the formalism has led to notable contributions to the engineering of critical systems,compilers , concurrent systems and inlogic forcomputer science .Philosophy
Computing systems may be modeled in VDM-SL at a higher level of abstraction than is achievable using programming languages, allowing the analysis of designs and identification of key features, including defects, at an early stage of system development. Models that have been validated can be transformed into detailed system designs through a refinement process. The language has a formal semantics, enabling proof of the properties of models to a high level of assurance. It also has an executable subset, so that models may be analyzed by testing and can be executed through graphical user interfaces, so that models can be evaluated by experts who are not necessarily familiar with the modeling language itself.
History
The origins of VDM-SL lie in the
IBM Laboratory inVienna where the first version of the language was called the Vienna Definition Language (VDL). [Bjørner&Jones 1978, p.ix] The VDL was essentially used for giving [http://en.wikipedia.org/wiki/Operational_semantics operational semantics] descriptions in contrast to the VDM - Meta-IV which provided [http://en.wikipedia.org/wiki/Denotational_semantics denotational semantics] [Introductory remarks by Cliff B. Jones (editor) in Bekič 1984, p.vii]«Towards the end of 1972 the Vienna group again turned their attention to the problem of systematically developing a compiler from a language definition. The overall approach adopted has been termed the "Vienna Development Method"... The meta-language actually adopted ("Meta-IV") is used to define major portions of PL/1 (as given in ECMA 74 - interestingly a "formal standards document written as an abstract interpreter) in BEKIČ 74.» [Bjørner&Jones 1978, p.xi]
So
Meta-IV [Bjørner&Jones 1978, p.24.] , was "used to define major portions of" thePL/I programming language. Other programming languages described, or partially described, using Meta-IV and VDM-SL include theBASIC programming language ,FORTRAN , theAPL programming language ,ALGOL 60, theAda programming language and thePascal programming language . Meta-IV evolved into several variants, generally described as the Danish, English and Irish Schools.The "English School" derived from work by Cliff Jones on the aspects of VDM not specifically related to language definition and compiler design (Jones 1980, 1990). It stresses modelling persistent [See the article on [http://en.wikipedia.org/wiki/Persistence_(computer_science) persistence] for its use within computer science.] state through the use of data types constructed from a rich collection of base types. Functionality is typically described through operations which may have side-effects on the state and which are mostly specified implicitly using a precondition and postcondition. The "Danish School" (Bjørner "et al." 1982) has tended to stress a constructive approach with explicit operational specification used to a greater extent. Work in the Danish school led to the first European validated Ada compiler.
An ISO Standard for the language was released in 1996 (ISO, 1996).
VDM Features
The VDM-SL and VDM++ syntax and semantics are described at length in the VDMTools language manuals and in the available texts. The ISO Standard contains a formal definition of the language’s semantics. In the remainder of this article, the ISO-defined interchange (ASCII) syntax is used. Some texts prefer a more concise mathematical syntax.
A VDM-SL model is a system description given in terms of the functionality performed on data. It consists of a series of definitions of data types and functions or operations performed upon them.
Basic Types: numeric, character, token and quote types
VDM-SL includes basic types modelling numbers and characters as follows:
The finite sequence type constructor (written
seq of T
whereT
is a predefined type) constructs the type composed of all finite lists of values drawn from the typeT
. For example, the type definitionString = seq of char
Defines a type
String
composed of all finite strings of characters. Various operators are defined on sequences for constructing concatenation, selection of elements and subsequences etc. Many of these operators are partial in the sense that they are not defined for certain applications. For example, selecting the 5th element of a sequence that contains only three elements is undefined.The order and repetition of items in a sequence is significant, so
[a, b]
is not equal to[b, a]
, and[a]
is not equal to[a, a]
.Data reification
Data reification (stepwise refinement) involves finding a more concrete representation of the abstract data types used in a specification. There may be several steps before an implementation is reached. Each reification step for an abstract data representation
ABS_REP
involves proposing a new representationNEW_REP
. In order to show that the new representation is accurate, a "retrieve function" is defined that relatesNEW_REP
toABS_REP
, i.e.retr : NEW_REP -> ABS_REP
. The correctness of a data reification depends on proving "adequacy", i.e.forall a:ABS_REP & exists r:NEW_REP & a = retr(r)
Since the data representation has changed, it is necessary to update the operations and functions so that they operate on
NEW_REP
. The new operations and functions should be shown to preserve any data typeinvariant s on the new representation. In order to prove that the new operations and functions model those found in the original specification, it is necessary to discharge two proof obligations:
* Domain rule: forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)
* Modelling rule: forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r))Example data reification
In a business security system, workers are given ID cards; these are fed into card readers on entry to and exit from the factory.Operations required:
*INIT()
initialises the system, assumes that the factory is empty
*ENTER(p : Person)
records that a worker is entering the factory; the workers' details are read from the ID card)
*EXIT(p : Person)
records that a worker is exiting the factory
*IS-PRESENT(p : Person) r : bool
checks to see if a specified worker is in the factory or notFormally, this would be:
types Person = token; Workers = set of Person; state AWCCS of pres: Workers end operations INIT() ext wr pres: Workers post pres = {}; ENTER(p : Person) ext wr pres : Workers pre p not in set pres post pres = pres~ union {p}; EXIT(p : Person) ext wr pres : Workers pre p in set pres post pres = pres~{p}; ISPRESENT(p : Person) r : bool ext rd pres : Workers post r <=> p in set pres~
As most programming languages have a concept comparable to a set (often in the form of an array), the first step from the specification is to represent the data in terms of a sequence. These sequences must not allow repetition, as we do not want the same worker to appear twice, so we must add an
invariant to the new data type. In this case, ordering is not important, so[a,b]
is the same as[b,a]
.The Vienna Development Method is valuable for model-based systems. It is not appropriate if the system is time-based. For such cases, the
calculus of communicating systems (CCS) is more useful.References
Reading Links
- cite book | last = Bjørner | first = Dines | authorlink = | coauthors = Cliff B. Jones | title = The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science 61 | publisher = Springer | date = 1978 | location = Berlin, Heidelberg, New York | pages = | url = | doi = | id = | isbn = 3-540-08766-4, ISBN 0-387-08766-4
- cite book | last = O'Regan | first = Gerard | authorlink = | coauthors = | title = Mathematical Approaches to Software Quality | publisher = Springer | date = 2006 | location = London | pages = | url = | doi = | id = | isbn = 978-1-84628-242-3
- cite book | last = Bekič | first = Hans | authorlink = | coauthors = Cliff B. Jones (editor) | title = Programming Languages and Their Definition, Lecture Notes in Computer Science 177 | publisher = Springer-Verlag | date = 1984 | location = Berlin, Heidelberg, New York, Tokyo | pages = | url = | doi = | id = | isbn = 3-540-13378-X
* Fitzgerald, J.S. and Larsen, P.G., "Modelling Systems: Practical Tools and Techniques in Software Engineering".
Cambridge University Press , 1998 ISBN 0-521-62348-0 (Japanese Edition pub.Iwanami Shoten 2003 ISBN 4-00-005609-3). [ [http://www.csr.ncl.ac.uk/modelling-book/ "Modelling Systems: Practical Tools and Techniques in Software Engineering"] ]
* Fitzgerald, J.S., Larsen, P.G., Mukherjee, P., Plat, N. and Verhoef,M., "Validated Designs for Object-oriented Systems".Springer Verlag 2005. ISBN 1-85233-881-4. Supporting web site [http://www.vdmbook.com] includes examples and free tool support. [ [http://www.vdmbook.com/ "Validated Designs for Object-oriented Systems"]
* Jones, C.B., "Systematic Software Development using VDM",Prentice Hall 1990. ISBN 0-13-880733-7. Also available on-line and free of charge: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip
* Bjørner, D. and Jones, C.B., "Formal Specification and Software Development"Prentice Hall International, 1982. ISBN 0-13-880733-7
* J. Dawes, "The VDM-SL Reference Guide",Pitman 1991. ISBN 0-273-03151-1
*International Organization for Standardization , "Information technology — Programming languages, their environments and system software interfaces — Vienna Development Method — Specification Language — Part 1: Base language" International Standard ISO/IEC 13817-1, December 1996.
* Jones, C.B., "Software Development: A Rigorous Approach", Prentice Hall International, 1980. ISBN 0-13-821884-6
* Jones, C.B. and Shaw, R.C. (eds.), "Case Studies in Systematic Software Development", Prentice Hall International, 1990. ISBN 0-13-880733-7
* Bicarregui, J.C., Fitzgerald, J.S., Lindsay, P.A., Moore, R. and Ritchie, B., "Proof in VDM: a Practitioner's Guide".Springer Verlag Formal Approaches to Computing and Information Technology (FACIT), 1994. ISBN 3-540-19813-X .External links
* [http://www.vdmportal.org/ Information on VDM and VDM++]
* [http://hopl.murdoch.edu.au/showlanguage2.prx?exp=598 Vienna Definition Language (VDL)]ee also
*
Formal methods
*Formal specification
*Predicate logic
*Propositional calculus
*Z specification language , the main alternative to VDM-SL (compare)
*Pidgin code
Wikimedia Foundation. 2010.