Tim Miller

Email: username tmiller at the domain unimelb dot edu dot au

Short Abstract: (click here for the full 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 project 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.

Project Outputs:

Tim Miller and Paul Strooper. Animation Can Show Only the Presence of Errors, Never Their Absence. Proc. of the 2001 Australian Software Engineering Conference (ASWEC 2001), pages 76-85, IEEE Computer Society, 2001.

Tim Miller and Paul Strooper. Combining the Animation and Testing of Abstract Data Types Proc. of the Second Asia-Pacific Conference on Quality Software (APAQS), pages 249-258, IEEE Computer Society, 2001.

Tim Miller and Paul Strooper. Model-Based Specification Animation Using Testgraphs. Proc. of the International Conference on Formal Engineering Methods (ICFEM), pages 192-203, Springer-Verlag, 2002.

Tim Miller and Paul Strooper. Supporting the Software Testing Process Specification Animation. Proc. of the First International Conference on Software Engineering and Formal Methods, pages 14-23, IEEE Computer Society, 2003.

Tim Miller and Paul Strooper. A Framework for the Systematic Testing of Model-Based Specifications. ACM Transactions on Software Engineering and Methodology, 12(4):409-439, October, 2003

Tim Miller and Paul Strooper. A Case Study in Specification and Implementation Testing. Proc. of the Asia Pacific Software Engineering Conference (APSEC'04), pages 130-139, IEEE Computer Society, 2004.

Tim Miller and Paul Strooper. A case study in model-based testing of specifications and implementations. Software Testing, Verification, and Reliability, 22(1):33-63, 2012.

Software:

A GNU/Linux version of the Possum animator that includes the testgraph editor.

The original version of Possum can be downloaded for GNU/Linux or Solaris.

Examples. Examples of testing a specification using animation, and testing the implementation of that specification using animation. Unzip the file examples.tgz. This will create a directory called 'examples', which contains two sub-directories 'animation' and 'testing'. These both contain README.txt files that give directions on how to build and run the examples.

The GSM 11.11 case study. The source for the entire GSM case study, including specification testing, implementation testing, and mutation analysis. Unzip the file gsm.tgz. This will create a directory called 'gsm', which contains a README.txt file that gives directions on how to build and run the examples and the mutation analysis.