Pilbrow, C., & Reeves, S. (2015). Using state machines for the visualisation of specifications via refinement. In Proceedings of the ASWEC 2015 24th Australasian Software Engineering Conference (Vol. II, pp. 106–110). New York, USA: ACM. http://doi.org/10.1145/2811681.2811702
Permanent Research Commons link: https://hdl.handle.net/10289/9795
We talk in this paper about using state machines and refinement to characterise the visualisation of a computation. We use Z specifications to give examples of systems in the usual way, and then use Z schemas to also represent states and transitions in state machines, which we consider to be a particular kind of visualisation of a specified system. We have investigated the principle of substitutivity and the idea of downward simulation to check whether or not a refinement relation exists between the specification and the state machine. We are looking at this because we believe that the soundness of the visualisation can be captured by such a refinement relationship.
© 2015 Copyright held by the owner/author(s). Publication rights licensed to ACM.