Abstract
Achieving consistency between a specification and its implementation is an important part of software development. In this paper, we present a method for generating passive test oracles that act as self-checking implementations. The implementation is verified using an animation tool to check that the behaviour of the implementation matches the behaviour of the specification. We discuss how to integrate this method into a framework developed for systematically animating specifications, which means a tester can significantly reduce testing time and effort by reusing work products from the animation. One such work product is a test-graph: a directed graph that partially models the states and transitions of the specification. Test-graphs are used to generate sequences for animation, and during testing, to execute these same sequences on the implementation.