Formal Verification of UML Statecharts with Real-time Extensions

Alexandre David, M. Oliver Möller, Wang Yi

Extended Abstract:


We present a framework for formal verification of a real-time extension of UML
statecharts.  This formalism is based on hierarchical state machines, that can
be put in parallel at any level of composition. It features powerful
event-communication, synchronization mechanisms, and actions triggered on
entry or exit of components. Industrial modeling tools like Rhapsody or
Rational Rose support UML statecharts and are applied in large-scale projects.

We restrict ourselves to the subset, where synchronization happens only in
hand-shake fashion and actions are always associated with transitions.  Then
we enrich this subset with with real-time constructs, namely clocks, timed
guards, and invariants. This makes the modeling language appropriate for
systems, where the correct behavior is dependent on time constraints and
subtle synchronization of individual components via delays.

In the  formal analysis, it is then e.g. not only possible to establish, that
every action a is necessarily followed by an action b, it can also be
proven (or refuted) that this happens within some fixed time bound.


We formally describe the such obtained modeling language as hierarchical timed
automata (HTAs), and equip it with a rule-based formal semantics.  Properties
of a model in this formalism can be expressed in real-time logics like timed
computation tree logic (TCTL).  To realize automated verification, we give a
translation of HTAs into a network of flat timed automata with hand-shake
synchronization, basic data types, and committed locations.  This can serve as
input to the UPPAAL model checking tool.


We report on an XML based implementation of this translation.  The well-known
pacemaker example is used to illustrate our technique: we are able to
model-check safety and (unbounded) response properties. It turns out that the
validity of a safety property is strongly dependent on the right choice of
parameters. Here, the results of the formal verification can be used to make
correcting adjustments in the model. 

For translation and verification we give run-time data.
An detailed exposition of this work is available in a technical
report.