Hierarchical Communicating Real-Time State Machines (H-CRSM) is a formal modelling language for the modular development of distributed real-time systems. The formalism is characterized by the use of state transitions with guarded commands and timing constraints, the adoption of a few distilled statecharts constructs, and the modular specification of timing constraints along a state hierarchy. This paper proposes a translation of H-CRSM into UPPAAL which enables model checking. Translation rests on unfolding a hierarchical model on a flat representation.
Model Checking Hierarchical Communicating Real-Time State Machines
FURFARO, Angelo;Nigro L.
2005-01-01
Abstract
Hierarchical Communicating Real-Time State Machines (H-CRSM) is a formal modelling language for the modular development of distributed real-time systems. The formalism is characterized by the use of state transitions with guarded commands and timing constraints, the adoption of a few distilled statecharts constructs, and the modular specification of timing constraints along a state hierarchy. This paper proposes a translation of H-CRSM into UPPAAL which enables model checking. Translation rests on unfolding a hierarchical model on a flat representation.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.