Using Specification Animation to support Specification Testing and Software Testing

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 {\em 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.