A Framework for Systematic Specification Animation

Miller, Tim and Strooper, Paul (2002) A Framework for Systematic Specification Animation. Technical Report 02-35, Software Verification Research Centre, School of Information Technology, The University of Queensland.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
svrc_02_35.pdf svrc_02_35.pdf application/pdf 343.10KB 198
svrc_02_35.ps svrc_02_35.ps Click to show the corresponding preview/stream application/postscript 310.63KB 128
Author Miller, Tim
Strooper, Paul
Title A Framework for Systematic Specification Animation
School, Department or Centre Software Verification Research Centre, School of Information Technology
Institution The University of Queensland
Report Number Technical Report 02-35
Publication date 2002-09-01
Subject 280302 Software Engineering
Abstract/Summary Specification animation allows users to pose questions about specifications that can be answered quickly and automatically. This paper presents a framework for systematically animating specifications. Several generic properties are identified to check on specifications. A method is presented that uses variants of the specification to check these properties using an animation tool, and also uses testgraphs (directed graphs that partially model the specification being animated) to check the properties for a large number of interesting states. Tool support for all of the above is also discussed. The framework is demonstrated on a small specification and its application to two larger specifications is discussed. Experience with the framework indicates that it can be used to effectively animate small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.
Keyword Specification animation
testing
formal specification
Additional Notes This paper has been submitted to Transactions on Software Engineering and Methodology.

Document type: Department Technical Report
Collection: School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 294 Abstract Views, 326 File Downloads  -  Detailed Statistics
Created: Thu, 08 Apr 2004, 10:00:00 EST by Belinda Weaver (EA)