Modelling and Verification of Real-Time Publish and Subscribe Protocol Using U ppaal and Simulink/Stateflow
- PDF / 2,764,276 Bytes
- 19 Pages / 595 x 842 pts (A4) Page_size
- 95 Downloads / 233 Views
Modelling and Verification of Real-Time Publish and Subscribe Protocol Using UPPAAL and Simulink/Stateflow Qian-Qian Lin1 , Shu-Ling Wang1 , Member, CCF, Bo-Hua Zhan1 , Member, CCF, and Bin Gu2,∗ , Member, CCF 1 2
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China Beijing Institute of Control Engineering, Beijing 100081, China
E-mail: {linqq, wangsl, bzhan}@ios.ac.cn; [email protected] Received April 11, 2020; revised October 10, 2020. Abstract 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 simulation, 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. Keywords
1
Real-Time Publish and Subscribe (RTPS), modelling, verification, Uppaal, Simulink/Stateflow
Introduction
Data distribution service (DDS) [1] is a portable middleware technology which provides an interface of information transmission among applications and operating systems. Adopting the Publish/Subscribe architecture, DDS takes data as the center, and provides the rich QoS (quality of service) strategy to realize data management and data sharing in the whole network [2] . It is widely used in aerospace and national defense fields requiring high performance, predictability and effective use of resources. The Real-Time Publish and Subscribe (RTPS) protocol [3, 4] has been standardized by the OMG (Object Management Group) as an interoperability protocol implemented using DDS. The protocol specifies requirements that any implementation must satisfy in order to be interoperable with each
other. These include the structure of entities involved in the conversation network, format for messages and their exchange ways, and a mechanism for discovering other participants. The protocol allows flexibility in the implementation, including the choice of best-effort or reliable communication, and the state to keep at the endpoints. In this paper, we build formal models for the RTPS protocol using Simulink/Stateflow and Uppaal. The models describe detailed behaviors specified by the protocol, including its real-t
Data Loading...
