TY - GEN
T1 - Transforming RoboSim Models into UPPAAL
AU - Zhang, Mingzhuo
AU - Du, Dehui
AU - Sampaio, Augusto
AU - Cavalcanti, Ana
AU - Filho, Madiel Conserva
AU - Zhang, Menghan
N1 - Publisher Copyright:
© 2021 IEEE.
PY - 2021/8
Y1 - 2021/8
N2 - RoboSim is a tool-independent notation for modeling software simulations of robots, and it can be verified by a variety of techniques and tools, including model checking and theorem proving. RoboSim has a formal tock-CSP (Communicating Sequential Processes) semantics, and so refinement checkers, such as FDR, can be used for verification of models. In this paper, we explore the use of UPPAAL, as a well-established tool for verification of time-dependent properties. We propose a model-transformation strategy to translate RoboSim models into NTA (Network of Timed Automata) based on some patterns and mapping rules. We implement our strategy as a plug-in for the RoboSim modeling and verification tool. Using examples, we compare the verification results of UPPAAL and FDR for a series of safety, reachability, and liveness properties. Moreover, we use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our approach can be extended to the verification of stochastic and hybrid systems using UPPAAL SMC. Such an extension cannot be easily conceived for The original tock-CSP semantics of RoboSim.
AB - RoboSim is a tool-independent notation for modeling software simulations of robots, and it can be verified by a variety of techniques and tools, including model checking and theorem proving. RoboSim has a formal tock-CSP (Communicating Sequential Processes) semantics, and so refinement checkers, such as FDR, can be used for verification of models. In this paper, we explore the use of UPPAAL, as a well-established tool for verification of time-dependent properties. We propose a model-transformation strategy to translate RoboSim models into NTA (Network of Timed Automata) based on some patterns and mapping rules. We implement our strategy as a plug-in for the RoboSim modeling and verification tool. Using examples, we compare the verification results of UPPAAL and FDR for a series of safety, reachability, and liveness properties. Moreover, we use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our approach can be extended to the verification of stochastic and hybrid systems using UPPAAL SMC. Such an extension cannot be easily conceived for The original tock-CSP semantics of RoboSim.
KW - CSP
KW - Model transformation
KW - Patterns
KW - Rules
KW - Timed Automata
KW - UPPAAL
UR - https://www.scopus.com/pages/publications/85116864389
U2 - 10.1109/TASE52547.2021.00037
DO - 10.1109/TASE52547.2021.00037
M3 - 会议稿件
AN - SCOPUS:85116864389
T3 - Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
SP - 79
EP - 86
BT - Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 15th International Symposium on Theoretical Aspects of Software Engineering, TASE 2021
Y2 - 25 August 2021 through 27 August 2021
ER -