Automatic Test Data Generation From VDM-SL Specifications
What is it?
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.
What does it do?
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.
About Formal Methods
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:
- Formal specification: The behaviour of each function, class etc. is specified in a quite abstract, mathematical way, mainly using predicate expressions. The languages used for this are very powerful; for example, they support quantifiers. The most popular languages appear to be Z and VDM-SL.
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.
Program and Dissertation
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.
- Update: Someone noticed that vdmpart no longer compiles with newer versions of GCC. Here is a patch for GCC 3.3: vdmpart-1.0.0-040316.diff
- The archive above contains the dissertation, but LaTeX is
needed to generate it. However, the dissertation is also available
as PDF and PostScript:
Related Documents
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:
To top - Unless noted otherwise, all graphics, programs and text © Copyright 2010 Richard Atterer. All trademarks are the property of their respective owners.