Temporal verification of communicating real-time state machines using Uppaal

Communicating real-time state machines (CRSM) are a formal modelling language for the development of distributed real-time systems. This paper proposes a mapping from CRSM to timed automata in the context of the Uppaal tool, with the purpose of enabling temporal validation and verification activities respectively based on simulation and model checking of a CRSM system. Usefulness and limitations of the mapping process are demonstrated through the verification of a real-time modelling example.