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.
Temporal verification of Communicating Real-Time State Machines using Uppaal
FURFARO, Angelo;Nigro L.
2003-01-01
Abstract
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
