Using specification animation to support specification testing and software testing

Timothy Miller (2005). Using specification animation to support specification testing and software testing PhD Thesis, School of Information Technology and Electrical Engineering, The University of Queensland.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
THE18489.pdf Full text application/pdf 9.62MB 5
Author Timothy Miller
Thesis Title Using specification animation to support specification testing and software testing
School, Centre or Institute School of Information Technology and Electrical Engineering
Institution The University of Queensland
Publication date 2005
Thesis type PhD Thesis
Supervisor A/Prof Paul Strooper
Dr. Colin Fidge
Total pages 292
Language eng
Subjects 0803 Computer Software
0899 Other Information and Computing Sciences
Formatted abstract

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. 

Keyword Computer animation
Computer software -- Development
Computer software -- Verification
Computer software -- Validation
Computer software -- Specifications -- Testing

Document type: Thesis
Collection: UQ Theses (RHD) - UQ staff and students only
Citation counts: Google Scholar Search Google Scholar
Created: Tue, 19 Jun 2012, 18:17:27 EST by Talha Alam on behalf of The University of Queensland Library