We develop a formal model for hierarchical timed systems. The statechart-like hierarchy features parallelism on any level and connects superstate and substate via explicit entries and exits. Time is represented by clocks, invariants, and guards. For this formalism we give an operational semantics that is appropriate for the verification of universal timed computation tree logic (TCTL) properties.
Our model is strongly related to the timed automata dialect as present in the model checking tool UPPAAL. Here networks of timed automata are enriched with shared variables, hand-shake synchronization, and urgency.
We describe a flattening procedure that translates our formalism into a network of UPPAAL timed automata. This flattening preserves a correspondence of the sets of legal traces. Therefor the translation can be used to establish properties in the hierarchical model.
As a case study, we use the standard UML modeling example of a cardiac pacemaker. We model it in our hierarchical language, flatten it to UPPAAL input, and use the latter for a formal analysis.
Our formalism remains decidable with respect to TCTL properties. In general the encoding of statecharts requires an abstraction step, which is not covered by this article.
Download BibTeX entry.