Model checking hierarchical communicating real-time state machines
| Title | Model checking hierarchical communicating real-time state machines |
| Publication Type | Conference Paper |
| Year of Publication | 2005 |
| Authors | Furfaro, A, Nigro, L |
| Conference Name | Emerging Technologies and Factory Automation, 2005. ETFA 2005. 10th IEEE Conference on |
| Pagination | 6 pp.-370 |
| Date Published | Sept |
| Keywords | Automata, Automatic control, Computational modeling, Control system synthesis, finite state machines, formal languages, formal modelling language, formal specification, H-CRSM, hierarchical communicating real-time state machine, model checking, modular specification, Prototypes, Real time systems, Real-time systems, specification languages, Time factors, Timing, timing constraint, UPPAAL |
| 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 |
| DOI | 10.1109/ETFA.2005.1612546 |