Tools for Real-Time UML: Formal Verification and Code Synthesis

(Tobias Amnell, Alexandre David, Elena Fersman, M. Oliver Möller, Paul
 Petterson, and Wany Yi)

Abstract:

  We present a real-time extension of UML statecharts to enable modelling and
  verification of real-timed constraints.  For clarity, we shall consider a
  reasonable subset of the rich UML statechart model and extend it with
  real-time constructs (clocks, timed guards, invariants and real-time tasks).
  We have developed a a rule-based formal semantics for the obtained
  formalism, called hierarchical timed automata (HTA). To use the existing
  tool UPPAAL for formal verification, HTA are translated to enriched timed
  automata model.

  We report on an XML based implementation of the translation from
  HTA to a network of timed automata and present an example to
  illustrate our technique and report run-time data for the formal
  verification part. We also report on a prototype implementation of
  the code synthesis for the {\it legOS} platform.