Model checking hierarchical communicating real-time state machines

TitleModel checking hierarchical communicating real-time state machines
Publication TypeConference Paper
Year of Publication2005
AuthorsFurfaro, A, Nigro, L
Conference NameEmerging Technologies and Factory Automation, 2005. ETFA 2005. 10th IEEE Conference on
Pagination6 pp.-370
Date PublishedSept
KeywordsAutomata, 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

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