Modelling and Verification of Real-Time Publish and Subscribe Protocol Using UPPAAL and Simulink/Stateflow  

作　　者：Qian-Qian Lin Shu-Ling Wang Bo-Hua Zhan Bin Gu 

机构地区：[1]State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China [2]Beijing Institute of Control Engineering,Beijing 100081,China

出　　处：《Journal of Computer Science & Technology》2020年第6期1324-1342,共19页计算机科学技术学报（英文版）

基　　金：This work was partially supported by the National Natural Science Foundation of China under Grant Nos.61625206,61972385 and 61732001;the 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.

关 键 词：Real-Time Publish and Subscribe(RTPS) MODELLING VERIFICATION UPPAAL Simulink/Stateflow 

分 类 号：TP39[自动化与计算机技术—计算机应用技术]