TY - GEN
T1 - Formal verification of uml statecharts with real-time extensions
AU - David, Alexandre
AU - Oliver Möller, M.
AU - Yi, Wang
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84958778942
U2 - 10.1007/3-540-45923-5_15
DO - 10.1007/3-540-45923-5_15
M3 - 会议稿件
AN - SCOPUS:84958778942
SN - 3540433538
SN - 9783540433538
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 218
EP - 232
BT - Fundamental Approaches to Software Engineering - 5th International Conference, FASE 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002 Proceedings
A2 - Kutsche, Ralf-Detlef
A2 - Weber, Herbert
PB - Springer Verlag
T2 - 5th International Conference on Fundamental Approaches to Software Engineering, FASE 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002
Y2 - 8 April 2002 through 12 April 2002
ER -