Automatic Test Data Generation From VDM-SL Specifications
This program and the accompanying dissertation are the result of a software engineering project I did in the 1999/2000 term while studying abroad at the Queen's University of Belfast (Northern Ireland) for one year. The project involved the specification, design, implementation and testing of a program, as well as a presentation of the final result.
The program vdmpart should be regarded as
experimental; it is hardly useful without (a lot of) further
work. However, it might be of interest to anybody who is acquainted
with VDM-SL, the Specification Language of the Vienna Development
Model, or is interested in Formal Methods.
Below is a short description of the term formal methods, and an
explanation of why a tool similar to vdmpart is
needed. For a more detailed description of the program, see the
introduction and specification sections of the dissertation.
Formal methods are the attempt to avoid some of the problems encountered when developing very large computer programs, such as inappropriate interfaces between components, insufficient documentation from which an implementer cannot tell exactly what behaviour the developer expected, and the difficulty of finding bugs resulting from this. There are two major aspects to formal methods:
Verified design: After the abstract specification of the component has been written, it is transformed (possibly with intermediate steps) into a form that more closely resembles a programming language (e.g. not containing any quantifiers). For each such transformation, it is proven that the two ways of describing the behaviour are equivalent.
At the end, when the component can be described by something that can be expressed directly in a programming language such as Java, there is a mathematical proof that the code satisfies the abstract specification.
Ideally, all the proofs would be performed by a program and the final code would not need any testing since it is known to satisfy the specification. However, in practice there are a number of problems. While the majority of the proofs can be automated, some need human assistance to solve, and that human can make mistakes. Furthermore, it is also possible that the abstract specification contains mistakes which could not be detected automatically. Thus, tests of the final program are as important as with conventionally developed software.
Fortunately, when testing software developed with formal methods, one has the advantage that both an abstract specification and an implementation is available. This makes it possible to test for bugs in places where they are most likely, and, very importantly, to automate testing.
The basic approach taken by a test data generation tool is to look at the abstract specification, determine values for inputs (e.g. function arguments) and corresponding outputs, and to execute the code with these inputs, comparing the actual and desired outputs. As before, the power of the specification language makes full automation of the test data generation very difficult, if not impossible, but at least for a subset of the language, such a tool can be written.
If formal methods are so wonderful, why doesn't anybody seem to use them? Formal methods have been used for software with very high quality demands, but indeed, they are not popular at all. The main reasons for this are (in my opinion) the quite significant amount of additional work, and the mathematics involved.
The program is only available as source code. To compile it,
a Unix-like operating system or the CygWin environment
under Windows is needed. The source code is distributed under the
terms of the GNU GPL.
The program is based on the Ph.D. thesis of Christophe Meudec,
which is available from
his homepage or from this page:
The VDM Specification Language is described in a 1993 ISO draft. That draft has since been superseded, but the final standard is not available for free, so the program is based on the draft.
Update: Unfortunately, the draft version seems to have completely dropped off the net around 2002 or so. This is where it used to be available from: