Real-Time Publish and Subscribe (RTPS) protocol is a protocol for implementing message exchange over an unreliable transport in data distribution service (DDS). Formal modelling and verification of the protocol provid...Real-Time Publish and Subscribe (RTPS) protocol is a protocol for implementing message exchange over an unreliable transport in data distribution service (DDS). Formal modelling and verification of the protocol provide stronger guarantees of its correctness and efficiency than testing alone. In this paper, we build formal models for the RTPS protocol using UPPAAL and Simulink/Stateflow. Modelling using Simulink/Stateflow allows analyzing the protocol through simula-tion, as well as generate executable code. Modelling using UPPAAL allows us to verify properties of the model stated in TCTL (Timed Computation Tree Logic), as well as estimate its performance using statistical model checking. We further describe a procedure for translation from Stateflow to timed automata, where a subset of major features in Stateflow is supported, and prove the soundness statement that the Stateflow model is a refinement of the translated timed automata model. As a consequence, any property in a certain fragment of TCTL that we have verified for the timed automata model in UPPAAL is preserved for the original Stateflow model.展开更多
基金This work was partially supported by the National Natural Science Foundation of China under Grant Nos.61625206,61972385 and 61732001the Chinese Academy of Sciences Pioneer 100 Talents Program under Grant No.Y9RC585036.
文摘Real-Time Publish and Subscribe (RTPS) protocol is a protocol for implementing message exchange over an unreliable transport in data distribution service (DDS). Formal modelling and verification of the protocol provide stronger guarantees of its correctness and efficiency than testing alone. In this paper, we build formal models for the RTPS protocol using UPPAAL and Simulink/Stateflow. Modelling using Simulink/Stateflow allows analyzing the protocol through simula-tion, as well as generate executable code. Modelling using UPPAAL allows us to verify properties of the model stated in TCTL (Timed Computation Tree Logic), as well as estimate its performance using statistical model checking. We further describe a procedure for translation from Stateflow to timed automata, where a subset of major features in Stateflow is supported, and prove the soundness statement that the Stateflow model is a refinement of the translated timed automata model. As a consequence, any property in a certain fragment of TCTL that we have verified for the timed automata model in UPPAAL is preserved for the original Stateflow model.
