Abstract
The state machine paradigm is a popular and convenient means for expressing designs of critical systems. State machines can be readily represented by transition graphs, thus enhancing human understanding of even quite complex problems. In the case of state machines, tracing a path through the transition graph can represent a critical sequence in the execution of a machine. State machine notations are also amenable to formal treatment. A high-level of assurance can be gained by a combination of both these aspects: a machine-checked, formal proof together with a higher-level argument that can be understood by humans.
This paper describes proof tactics that support reasoning about state machines at the level of diagrams and paths, and the construction of a corresponding formal proof. A tool, called Veracity [3], has been developed, which links these powerful proof tactics to a graphical user-interface. The proof tactics are implemented in Isabelle, and the paper discusses some strengths and weaknesses of Isabelle as an appropriate base for modelling and proving properties of state machines.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
D. Basin, S. Matthews and L. Viganó. A modular presentation of modal logics in a logical framework. In Proceedings of the Tbilisi Symposium on Language, Logic and Computation, October 1995.
M. Bonsangue and J. N. Kok. Isomorphisms between predicate and state transfomers. In Mathematical Foundations of Computer Science, Volume 711 of LNCS. Springer-Verlag, 1993.
A. Cant, K. A. Eastaughffe and M. A. Ozols. A tool for practical reasoning about state machine designs. In Proc. 1996 Australian Software Engineering Conference, pages 16–26, Melbourne, July 1996. IEEE Computer Society Press.
A. Cant and M. A. Ozols. XIsabelle. Research Report RR-0008, Electronics and Surveillance Research Laboratory, DSTO, 1996.
D. Craigen et al. EVES: An Overview. Conference Paper CP-91-5402-43, Odyssey Research Associates, 265 Carling Avenue, Suite 506, Ottawa, Ontario, March 1991.
J. W. de Bakker. Recursive programs as predicate transformers. In Formal Description of Programming Concepts. North-Holland, 1978.
Kolyang, T. Santen and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In J. von Wright, J. Grundy and J. Harrison (editors), Proceedings of 9th International Conference on Theorem Proving in Higher-Order Logic, Volume 1125 of LNCS, pages 283–298. Springer-Verlag, 1996.
C. Owens. Coding binding and and substitution explicitly in Isabelle. Isabelle Users Workshop, Cambridge University, U.K., 1995.
S. Owre, J. M. Rushby and N. Shankar. PVS: A prototype verification system. In Deepak Kapur (editor), 11th International Conference on Automated Deduction (CADE), Volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer-Verlag.
M. A. Ozols, A. Cant and K. A. Eastaughffe. Xisabelle: System description. In 14th International Conference on Automated Deduction (CADE). Springer-Verlag, 1997.
L. C. Paulson and T. Nipkow. Isabelle: A Generic Theorem Prover, Volume 828 of LNCS. Springer Verlag, 1994.
A. Trybulec and H. A. Blair. Computer aided reasoning. In R. Parikh (editor), Logics of Programs, Volume 193 of LNCS, pages 406–412. Springer-Verlag, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eastaughffe, K.A., Ozols, M.A., Cant, A. (1997). Proof tactics for a theory of state machines in a graphical environment. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_35
Download citation
DOI: https://doi.org/10.1007/3-540-63104-6_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63104-0
Online ISBN: 978-3-540-69140-2
eBook Packages: Springer Book Archive