DocumentCode
409474
Title
Temporal verification of communicating real-time state machines using Uppaal
Author
Furfaro, Angelo ; Nigro, Libero
Author_Institution
Dipt. di Elettronica Informatica e Sistemistica, Calabria Univ., Rende, Italy
Volume
1
fYear
2003
fDate
10-12 Dec. 2003
Firstpage
399
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.
Keywords
automata theory; finite state machines; formal languages; real-time systems; communicating real-time state machines; distributed real-time systems; mapping process; temporal verification; timed automata; Automata; Context modeling; Formal languages; Laboratories; Prototypes; Real time systems; Robot kinematics; Robot sensing systems; Testing; Timing;
fLanguage
English
Publisher
ieee
Conference_Titel
Industrial Technology, 2003 IEEE International Conference on
Print_ISBN
0-7803-7852-0
Type
conf
DOI
10.1109/ICIT.2003.1290345
Filename
1290345
Link To Document