Timed Verification of Hierarchical Communicating Real-Time State Machines

TitleTimed Verification of Hierarchical Communicating Real-Time State Machines
Publication TypeJournal Article
Year of Publication2007
AuthorsFurfaro, A, Nigro, L
JournalComputer Standards & Interfaces
Volume29
Pagination635–646
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. The resultant approach is demonstrated by means of a case study.

DOI10.1016/j.csi.2007.04.003