|
Vienna Development Method (VDM) is a program development method based on formal specification using the VDM specification language (VDM-SL), with tool support. There is an object-oriented extension, VDM++.
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 types into more concrete data structures, while operation decomposition develops the (abstract) implicit specifications of operations and functions into algorithms 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: NEW_REP → ABS_REP 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: Person)— records that a worker is entering the factory; the workers' details are read from the ID card) Person)— records that a worker is exiting the factory Person) r— checks to see if a specified worker is in the factory or not Formally, this would be: types
state AWCCS of
endoperations
otin 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 Concurrent Calculus System (CCS) is more useful. Books | ||||||||
|
| |||||||||
 |
|
| |