A Framework for Systematic Specification Animation
Tim Miller, Paul A. Strooper · 2002
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.