Temporal verification of Communicating Real-Time State Machines using Uppaal
| Title | Temporal verification of Communicating Real-Time State Machines using Uppaal |
| Publication Type | Conference Paper |
| Year of Publication | 2003 |
| Authors | Furfaro, A, Nigro, L |
| Conference Name | Proc. of International Conference on Industrial Technology (IEEE-ICIT'03) |
| Date Published | December 10–12 |
| Publisher | IEEE Computer Society |
| Conference Location | Maribor, Slovenia |
| 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. |
| DOI | 10.1109/ICIT.2003.1290345 |