Modelling and Verification of Real-Time Publish and Subscribe Protocol Using UPPAAL and Simulink/Stateflow
作者机构：State Key Laboratory of Computer ScienceInstitute of SoftwareChinese Academy of SciencesBeijing 100190China Beijing Institute of Control EngineeringBeijing 100081China
出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)
年 卷 期：2020年第35卷第6期
页 面：1324-1342页
核心收录：
学科分类：081203[工学-计算机应用技术] 08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：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) modelling verification UPPAAL Simulink/Stateflow
摘 要：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.
维普期刊数据库