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:

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

Related Documents