We present a framework for formal verification of a real time extension of UML statecharts. For clarity, we restrict ourselves to a reasonable subset of the rich UML state chart model and extend this with real-time constructs (clocks, timed guards, and invariants). We equip the obtained formalism, called hierarchical timed automata (HTA), with an operational semantics. We outline a translation of one HTA to a network of flat timed automata, that can serve as input to the real-time model checking tool UPPAAL. This translation can be used to faithfully verify deadlock-freedom, safety, and unbounded response properties of the HTA model. We report on an XML-based implementation of this translation, use the well-known pacemaker example to illustrate our technique, and report run-time data for the formal verification part.
CITATION STYLE
David, A., Oliver Möller, M., & Yi, W. (2002). Formal verification of uml statecharts with real-time extensions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2306, pp. 218–232). Springer Verlag. https://doi.org/10.1007/3-540-45923-5_15
Mendeley helps you to discover research relevant for your work.