Formal specifications can precisely and unambiguously define the required behaviour of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent and complete, and validated to ensure that they fulfill their requirements. Current specification animation tools (or animators) can assist with specification testing by allowing a specification to be interpreted or executed. While not offering the same level of assurance as its more formal counterparts, such as theorem proving, specification testing is more straightforward and cheaper to perform. Despite the existence of a number of animators for a variety of languages, most of the literature simply mentions that a specification was tested, with no or little discussion of how this was done or how effective it was. As a result, little is known about how to effectively test specifications.
This thesis examines how to use specification animators to systematically test specifications, and then how to use the artifacts that are produced during the testing of a specification to support the testing of its implementation.
The first major contribution of this thesis is a framework for specification testing. Several generic properties to be checked on model-based specifications are identified. At the core of the framework are testgraphs: directed graphs that partially model the states and transitions of the specification. Testgraphs are used to model a subset of the behaviour of the specification, and then to generate sequences for testing. The framework also contains tool support to help with the more difficult and tedious parts of the testing process.
The second major contribution is the extension of this framework, focusing on the reuse of artifacts produced during the testing of a specification to support the testing of its implementation. The testgraph derived to test the specification is reused to test the implementation. The animator is also used to check the behaviour of the implementation. If the behaviour of the implementation does not match the behaviour of the specification, then an inconsistency between the specification and its implementation has been discovered.
Experience with the framework indicates that it can successfully be used for small to medium-sized systems, and that it can reveal a significant number of problems in both specifications and their corresponding implementations at a reasonable cost.