Formal Verification of UML Statecharts with Real-Time Extensions

(Alexandre David, M. Oliver Möllerma and  Wang Yi)

Abstract:

  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 statechart 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.