Abstract
Hierarchical Automata represent a structured model of statecharts. They are formalized in Isabelle/HOL. The formalization is on two levels. The first level is the set-based semantics; the second level exploits the tree-like structure of the hierarchical automata to represent them using Isabelle’s datatypes and primitive recursive functions. Thereby the proofs about hierarchical automata are simplified. In order to ensure soundness of this twofold approach we define a mapping from the latter to the former representation and prove that it preserves the defining properties of hierarchical automata.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
We’re sorry, something doesn't seem to be working properly.
Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.
References
J. Burghardt, F. Kammüller, J. Sanders. On the Antisymmetry of Galois Embeddings. Information Processing Letters, 79:2, Elsevier, June 2001.
P. Cousot and R. Cousot. Abstract Interpretation. In Principles of Programming Languages, ACM Press, 1977.
Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
Nancy Day and Jeffrey Joyce. The Semantics of Statecharts in HOL. In International Meeting on Higher-Order Logic Theorem Proving and its Applications. Springer LNCS, 780:338–351, 1993.
D. Harel and D. Naamad. A STATEMATE semantics for statecharts. ACM Trans. on Software Engineering and Methodology, 5(4):293–333, Oct 1996.
F. Kammüller and S. Helke. Mechanical Analysis of UML State Machines and Class Diagrams. In Defining Precise Semantics for UML, Sophia Antipolis, France, June 2000. Satellite Workshop, ECOOP 2000.
E. Mikk. Semantics and Verification of Statecharts. PhD thesis, Christian-Albrechts-Universität, Kiel. Bericht Nr. 2001, October 2000.
Olaf Müller and Tobias Nipkow. Combining Model Checking and Deduction for I/O Automata. In TACAS’95, Tools and Algorithms for the Construction and Analysis of Systems, Springer LNCS, 1019:1–16, 1995.
T. Nipkow and K. Slind. I/O Automata in Isabelle/HOL. In Types for Proofs and Programs, Springer LNCS, 996:101–119, 1995.
L. C. Paulson. Isabelle: A Generic Theorem Prover, Springer LNCS, 828, 1994.
Hassen Saïdi and Natarajan Shankar. Abstract and Model Check While You Prove. In N. Halbwachs and D. Peled, editors, 11th International Conference on Computer Aided Verification, CAV’99, Springer LNCS, 1633, 1999.
M. von der Beeck. A Comparison of Statechart Variants/ In Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer LNCS, 863: 128–148, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Helke, S., Kammüller, F. (2001). Representing Hierarchical Automata in Interactive Theorem Provers. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_17
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive