Using specification animation to support specification testing and software testing
Tim Miller · The University of Queensland · 2005
Formal specifications can precisely and unambiguously define the requirednbehaviour of a software system or component. However, formalnspecifications are complex artifacts that need to be verified to ensure thatnthey are consistent and complete, and validated to ensure that they fulfillntheir requirements. Current specification animation tools (or animators)ncan assist with specification testing by allowing a specification to be interpretednor executed. While not offering the same level of assurancenas its more formal counterparts, such as theorem proving, specificationntesting is more straightforward and cheaper to perform. Despite the existencenof a number of animators for a variety of languages, most of thenliterature simply mentions that a specification was tested, with no ornlittle discussion of how this was done or how effective it was. As a result,nlittle is known about how to effectively test specifications.n n This thesis examines how to use specification animators to systematicallyntest specifications, and then how to use the artifacts that are producednduring the testing of a specification to support the testing of its implementation.n n The first major contribution of this thesis is a framework for specificationntesting. Several generic properties to be checked on model-basednspecifications are identified. At the core of the framework are testgraphs:nndirected graphs that partially model the states and transitions of thenspecification. Testgraphs are used to model a subset of the behaviournof the specification, and then to generate sequences for testing. Thenframework also contains tool support to help with the more difficult andntedious parts of the testing process.n n The second major contribution is the extension of this framework, focusingnon the reuse of artifacts produced during the testing of a specificationnto support the testing of its implementation. The testgraph derived tontest the specification is reused to test the implementation. The animatornis also used to check the behaviour of the implementation. If thenbehaviour of the implementation does not match the behaviour of thenspecification, then an inconsistency between the specification and its implementationnhas been discovered.n n Experience with the framework indicates that it can successfully be usednfor small to medium-sized systems, and that it can reveal a significantnnumber of problems in both specifications and their corresponding implementationsnat a reasonable cost.n