First International Conference on Software Engineering and Formal Methods (SEFM'03)
Animation of Object-Z Specifications Using a Z Animator
Brisbane, Australia
September 22-September 27
ISBN: 0-7695-1949-0
We discuss a methodology for animating the Object-Z specification language using a Z animation environment. Central to the process is the introduction of a framework to handle dynamic instantiation of objects and management of object references. Particular focus is placed upon building the animation environment through pre-existing tools, and a case study is presented that implements the proposed framework using a shallow encoding in the Possum Z animator. The animation of Object-Z using Z is both automated and made transparent to the user through the use of a software tool named Ozone.