Vienna Development Method

THE DEVELOPMENT CYCLE

Use of VDM starts with a very Abstract specification and, develops this into an implementation. Each step involves Data Reification, then '''Operation Decomposition'''.

Data reification develops the Abstract Data Type s into more concrete Data Structure s, while operation decomposition develops the (abstract) implicit specifications of operations and functions into Algorithm s that can be directly implemented in a computer language of choice.

Data Reification

Data reification 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 step involves:

Given an abstract data representation "''ABS_REP''", find a new representation "''NEW_REP''".

Find a "retrieve function" that relates ''ABS_REP'' to ''NEW_REP'', i.e. ''retr : NEW_REP → ABS_REP''

Prove that ''NEW_REP'' is sufficient for representing ''ABS_REP'', i.e. prove that $orall a \in ABS\_REP \bullet \exists r \in NEW\_REP \bullet a = retr(r)$

Rewrite the operations and functions in terms of ''NEW_REP''

Prove that the new operations and functions preserve any data-type Invariant s of the new representation

Prove that the new operations and functions model those found in the original specification. This involves two rules:

--- Domain rule: $orall r \in NEW\_REP \bullet \mbox{pre-}OPA(retr(r)) \Rightarrow \mbox{pre-}OPR(r)$

--- Modelling rule: $orall \begin{matrix}\leftharpoonup \ r \end{matrix}, r \in NEW\_REP \bullet \mbox{pre-}OPA(retr(\begin{matrix}\leftharpoonup \ r \end{matrix})) \land \mbox{post-}OPR(\begin{matrix}\leftharpoonup \ r \end{matrix}, r) \Rightarrow \mbox{post-}OPA(retr(\begin{matrix}\leftharpoonup \ r \end{matrix}), 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 : $\mathbb{B}$ '' — checks to see if a specified worker is in the factory or not

Formally, this would be:

types

:''Person'' = To be defined

:''Workers'' = ''Person''-set

state ''AWCCS'' of

:''pres : Workers''

end

operations

:''INIT()''

:ext wr ''pres : Workers''

:post ''pres'' = {};

:''ENTER(p : Person)''

:ext wr ''pres : Workers''

:pre ''p $otin$ pres''

:post ''pres = $\begin{matrix}\leftharpoonup \ pres \end{matrix} \cup$ {p};''

:''EXIT(p : Person)''

:ext wr ''pres : Workers''

:pre ''p $\in$ pres''

:post ''pres = $\begin{matrix}\leftharpoonup \ pres \end{matrix}$ - {p};''

:''IS-PRESENT(p : Person) r : $\mathbb{B}$ ''

:ext rd ''pres : Workers''

:post ''r $\Leftrightarrow$ p $\in$ 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 ''b'' is the same as ''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 Concurrent Calculus System (CCS) is more useful.

EXTERNAL LINK

Information on VDM and VDM++

REFERENCES

Books

John Fitzgerald Et Al , Validated Designs for Object-oriented Systems, Springer Verlag 2005. ISBN 1852338814

John Fitzgerald et al, Modelling Systems, Cambridge University Press 1998. ISBN 0521626056

Cliff Jones , Systematic Software Development using VDM, Prentice Hall 1990. ISBN 0138807337. Also available on-line and free of charge: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip

Information About

Vienna Development Method