Abstract
The theory of Timed Transition Systems developed by Henzinger, Manna, and Pnueli provides a formal framework for specifying and reasoning about real-time systems. In this paper, we report on some preliminary investigations into the mechanization of this theory using the HOL theorem prover.
We review the main ideas of the theory and describe how it has been formally embedded in HOL. A graphical notation of timed transition diagrams and a real-time temporal logic for requirements have also been embedded in HOL using the embedding of timed transition systems. The proof rules proposed by Henzinger et al have been verified formally and we illustrate their use, as well as some problems we have encountered, by reference to a small example. More work is required on interfaces and proof methods to have a generally usable system.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
T.A. Henzinger, Z. Manna, and A Pnueli. Timed transition systems. InProceedings of the 1991 REX Workshop, November 1991.
SRI International and DSTO Australia.The HOL System Cambridge Computer Science Research Center, SRI International, revised version, 1991, (four volumes).
T.A. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for realtime systems. InProceedings of the 18th Symposium on Principles of Programming Languages, ACM Press, 1991.
R.J. Boulton. On efficiency in theorem provers which fully expand proofs into primitive inferences. Technical Report 248, Computer Laboratory, University of Cambridge, England, 1992.
T.A. Henzinger.The temporal specification and verification of real-time systems, PhD thesis, Department of Computer Science, Stanford University, California, 1991.
J.R. Harrison. Constructing the real numbers in HOL. InHigher Order Logic Theorem Proving and its Applications, eds L.J.M.Claesen and M.J.G. Gordon, North-Holland, 1992, 145–164.
Chin-Tsun Chow. A sequent formulation of a logic of predicates in HOL. InHigher Order Logic Theorem Proving and its Applications, L.J.M.Claesen and M.J.G.Gordon, eds., North-Holland, 1992, 71–80.
L. Théry, Y. Bertot, and G. Kahn. Real theorem provers deserve real user-interfaces. Technical Report 1684, INRIA, Sophia, Antipolis, 1992.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Hale, R., Cardell-Oliver, R. & Herbert, J. An embedding of Timed Transition Systems in HOL. Form Method Syst Des 3, 151–174 (1993). https://doi.org/10.1007/BF01383987
Issue Date:
DOI: https://doi.org/10.1007/BF01383987