Timed verification of hierarchical communicating real-time state machines |
| |
Authors: | Angelo Libero |
| |
Affiliation: | aDipartimento di Elettronica Informatica e Sistemistica Università della Calabria, I-87036 Rende (CS) — Italy |
| |
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. |
| |
Keywords: | Modelling Real-time systems Modularity constructs Timing constraints Model checking Timed automata U smCaps" >ppaal |
本文献已被 ScienceDirect 等数据库收录! |