Vienna Development Method

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 of object-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 in logic for computer 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 in Vienna 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" the PL/I programming language. Other programming languages described, or partially described, using Meta-IV and VDM-SL include the BASIC programming language, FORTRAN, the APL programming language, ALGOL 60, the Ada programming language and the Pascal 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 where T is a predefined type) constructs the type composed of all finite lists of values drawn from the type T. For example, the type definition

String = 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 representation NEW_REP. In order to show that the new representation is accurate, a "retrieve function" is defined that relates NEW_REP to ABS_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 type invariants 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 not

Formally, 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

  1. 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
  2. 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
  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.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • Vienna Development Method — (VDM) ist eine Methode zur Entwicklung von Computer Programmen, die auf formalen Spezifikationen mit Hilfe der VDM eigenen Spezifikationssprache Vienna Definition Language basiert. Es gibt eine objektorientierte Erweiterung, VDM++. Literatur John …   Deutsch Wikipedia

  • Vienna Development Method — El Vienna Development Method (VDM), en español, «Método de Desarrollo de Viena» es un método para el desarrollo de programas informáticos, que se base en especificaciones formales con ayuda del idioma de especificación propio Vienna Definition… …   Wikipedia Español

  • Vienna Development Method — Pour les articles homonymes, voir VDM. La Vienna Development Method, abrégé par le sigle VDM, est un ensemble d outils de développement informatique faisant appel à un grand formalisme. Une variante de la méthode VDM se nomme VDM++. Elle a été… …   Wikipédia en Français

  • Vienna Definition Language — Die Vienna Definition Language (VDL) ist eine im IBM Labor in Wien entwickelte Programmiersprache, die verwendet werden kann, um formale, algebraische Definitionen von Programmiersprachen für Computersoftware mit einer Operationellen Semantik… …   Deutsch Wikipedia

  • Vienna Definition Language — El Vienna Definition Language (VDL), en español, «Lenguaje de Definición de Viena» es un lenguaje de programación desarrollado en un centro de IBM en Viena (Austria), que puede utilizarse para declarar definiciones algebraicas de lenguajes de… …   Wikipedia Español

  • Vienna Circle — The Vienna Circle (in German: der Wiener Kreis) was a group of philosophers who gathered around Moritz Schlick when he was called to the Vienna University in 1922, organized in a philosophical association named Verein Ernst Mach (Ernst Mach… …   Wikipedia

  • Vienna School of Art History — The Vienna School of Art History ( Wiener Schule der Kunstgeschichte ) is a collective term used to describe the development of fundamental art historical methods at the University of Vienna. It does not describe a dogmatically unified group, but …   Wikipedia

  • Scientific method — …   Wikipedia

  • The Water-Method Man — Infobox Book | name = The Water Method Man title orig = translator = image caption = First edition cover author = John Irving illustrator = cover artist = country = United States language = English series = subject = genre = Novel publisher =… …   Wikipedia

  • University of Vienna —     University of Vienna     † Catholic Encyclopedia ► University of Vienna     Foundation of the University     Next to the University of Prague that of Vienna is the oldest university of the former Holy Roman Empire. It was founded on 12 March …   Catholic encyclopedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”