Journal of Computer Science and Technology ›› 2020, Vol. 35 ›› Issue (6): 1324-1342.doi: 10.1007/s11390-020-0537-8

Special Issue: Software Systems

Previous Articles     Next Articles

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. 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
  • Received:2020-04-11 Revised:2020-10-10 Online:2020-11-20 Published:2020-12-01
  • Contact: Bin Gu E-mail:gubinbj@sina.com
  • About author:Qian-Qian Lin received her Bachelor’s degree in electrical and information engineering from University of Science and Technology in China, Hefei, in 2017. She is currently a Master student at Institute of Software, Chinese Academy of Sciences, Beijing. Her research interests are modelling and simulation of embedded systems.
  • Supported by:
    This work was partially supported by the National Natural Science Foundation of China under Grant Nos. 61625206, 61972385 and 61732001, and the Chinese Academy of Sciences Pioneer 100 Talents Program under Grant No. Y9RC585036.

PDF (PC)

46

Supplement

1

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.

Key words: Real-Time Publish and Subscribe (RTPS); modelling; verification; Uppaal; Simulink/Stateflow;

[1] Andrès F, Boulos J. DDS:The data delivery service. In Proc. the IFIP World Conference on IT Tools, September 1996, pp.487-494.
[2] Hugues J, Pautet L, Kordon F. A framework for DRE middleware, an application to DDS. In Proc. the 9th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing, April 2006, pp.224-231.
[3] Almadani B. RTPS middleware for real-time distributed industrial vision systems. In Proc. the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, August 2005, pp.361-364.
[4] Almadani B, Al-Saeedi M, Al-Roubaiey A. Scalable wireless video streaming over real-time publish subscribe protocol (RTPS). In Proc. the 17th IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications, October 2013, pp.221-230.
[5] Behrmann G, David A, Larsen K G. A tutorial on UPPAAL. In Proc. International School on Formal Methods for the Design of Computer, Communication and Software Systems, September 2004, pp.200-236.
[6] David A, Larsen K G, Legay A, Mikucionis M, Poulsen D B. UPPAAL SMC tutorial. International Journal on Software Tools for Technology Transfer, 2015, 17(4):397-415.
[7] Beckman K, Reininger J. Adaptation of the DDS security standard for resource-constrained sensor networks. In Proc. the 13th International Symposium on Industrial Embedded Systems, June 2018.
[8] Youssef T A, Hariri M E, Elsayed A T, Mohammed O A. A DDS-based energy management framework for small microgrid operation and control. IEEE Trans. Industrial Informatics, 2018, 14(3):958-968.
[9] Pérez H, Gutiérrez J J. Modelling the QoS parameters of DDS for event-driven real-time applications. Journal of Systems and Software, 2015, 104:126-140.
[10] Alaerjan A, Kim D, Kafaf D A. Modeling functional behaviors of DDS. In Proc. the IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computed, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation, August 2017.
[11] Kleppe A. Object constraint language:Metamodeling semantics. In UML 2 Semantics and Applications, Lano K (ed.), Wiley, 2009, pp.163-178.
[12] Liu Y, Guan Y, Li X, Wang R, Zhang J. Formal analysis and verification of DDS in ROS2. In Proc. the 16th ACM/IEEE International Conference on Formal Methods and Models for System Design, October 2018, pp.62-66.
[13] Yin J, Zhu H, Fei W, Xu Q, Wu R. Formalization and verification of RTPS StatefulWriter module using CSP. In Proc. the 31st International Conference on Software Engineering and Knowledge Engineering, July 2019, pp.147-198.
[14] Brookes S D, Hoare C A R, Roscoe A W. A theory of communicating sequential processes. Journal of the ACM, 1984, 31(3):560-599.
[15] Hoare C A R. Communicating Sequential Processes. Prentice-Hall, 1985.
[16] Yang Y, Jiang Y, Gu M, Sun J. Verifying Simulink Stateflow model:Timed automata approach. In Proc. the 31st IEEE/ACM International Conference on Automated Software Engineering, September 2016, pp.852-857.
[17] Kang E, Ke L, Hua M, Wang Y. Verifying automotive systems in EAST-ADL/Stateflow using UPPAAL. In Proc. the 2015 Asia-Pacific Software Engineering Conference, December 2015, pp.143-150.
[18] Hamon G, Rushby J. An operational semantics for Stateflow. International Journal on Software Tools for Technology Transfer, 2007, 9(5/6):447-456.
[19] Tiwari A. Formal semantics and analysis methods for Simulink/Stateflow models. Technical Report, SRI International, 2002. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.3492, Mar. 2020.
[20] Zou L, Zhan N, Wang S, Fränzle M. Formal verification of Simulink/Stateflow diagrams. In Proc. the 13th International Symposium on Automated Technology for Verification and Analysis, October 2015, pp.464-481.
[21] Chen C, Sun J, Liu Y et al. Formal modeling and validation of Stateflow diagrams. International Journal on Software Tools for Technology Transfer, 2012, 14(6):653-671.
[22] Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2):183-235.
[23] Berhmann G, David A, Larsen K G, Pettersson P, Yi W. Developing UPPAAL over 15 years. Software-Practice and Experience, 2011, 41(2):133-142.
[24] Younes H L S, Kwiatkowska M, Normaln G, Parker D. Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer, 2007, 15(11):1427-1434.
[25] Georgios E F, George J P. Robust sampling for MITL specifications. In Proc. the 5th International Conference on Formal Modeling and Analysis of Timed Systems, Oct. 2007, pp.147-162.
[26] Grumberg O, Long D E. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 1994, 16(3):843-871.
[1] Zhi Ma, Lei Qiao, Meng-Fei Yang, Shao-Feng Li, Jin-Kun Zhang. Verification of Real Time Operating System Exception Management Based on SPARCv8 [J]. Journal of Computer Science and Technology, 2021, 36(6): 1367-1387.
[2] Jingwen Xu, Yanhong Huang, Jianqi Shi, Shengchao Qin. A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems [J]. Journal of Computer Science and Technology, 2021, 36(6): 1231-1247.
[3] Zhao-Hui Li, Xin-Yu Feng. Verifying Contextual Refinement with Ownership Transfer [J]. Journal of Computer Science and Technology, 2021, 36(6): 1342-1366.
[4] Jia-Qi Yin, Hui-Biao Zhu, Yuan Fei. Specification and Verification of the Zab Protocol with TLA+ [J]. Journal of Computer Science and Technology, 2020, 35(6): 1312-1323.
[5] Jun-Peng Zha, Xin-Yu Feng, Lei Qiao. Modular Verification of SPARCv8 Code [J]. Journal of Computer Science and Technology, 2020, 35(6): 1382-1405.
[6] Hui-Na Chao, Hua-Wei Li, Xiaoyu Song, Tian-Cheng Wang, Xiao-Wei Li. Evaluating and Constraining Hardware Assertions with Absent Scenarios [J]. Journal of Computer Science and Technology, 2020, 35(5): 1198-1216.
[7] Zi-Peng Zhang, Ming Fu, Xin-Yu Feng. A Lightweight Dynamic Enforcement of Privacy Protection for Android [J]. Journal of Computer Science and Technology, 2019, 34(4): 901-923.
[8] Wen-Min Li, Xue-Lei Li, Qiao-Yan Wen, Shuo Zhang, Hua Zhang. Flexible CP-ABE Based Access Control on Encrypted Data for Mobile Users in Hybrid Cloud System [J]. , 2017, 32(5): 974-990.
[9] Mert Ozkaya. Visual Specification and Analysis of Contract-Based Software Architectures [J]. , 2017, 32(5): 1025-1043.
[10] Peng-Yi Hao, Yang Xia, Xiao-Xin Li, Sei-ichiro Kamata, Sheng-Yong Chen. Discriminative Histogram Intersection Metric Learning and Its Applications [J]. , 2017, 32(3): 507-519.
[11] Cinzia Bernardeschi, Luca Cassano, Andrea Domenici. SRAM-Based FPGA Systems for Safety-Critical Applications: A Survey on Design Standards and Proposed Methodologies [J]. , 2015, 30(2): 373-390.
[12] Wen-Gang Zhou, Hou-Qiang Li, Yijuan Lu, Qi Tian. Encoding Spatial Context for Large-Scale Partial-DuplicateWeb Image Retrieval [J]. , 2014, 29(5): 837-848.
[13] Tao Xie, Lu Zhang, Xusheng Xiao, Ying-Fei Xiong, and Dan Hao. Cooperative Software Testing and Analysis：Advances and Challenges [J]. , 2014, 29(4): 713-723.
[14] Zhao-Peng Li, Yu Zhang, and Yi-Yun Chen. A Shape Graph Logic and A Shape System [J]. , 2013, 28(6): 1063-1084.
[15] Jun-Wei Cao, (曹军威), Member, CCF, ACM, Senior Member, IEEE, Fan Zhang (张帆), Student Member, IEEE, Ke Xu (许可), Lian-Chen Liu (刘连臣) and Cheng Wu (吴澄). Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows [J]. , 2011, 26(6): 1017-1030.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] Liu Mingye; Hong Enyu;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] Wang Xuan; Lü Zhimin; Tang Yuhai; Xiang Yang;. A High Resolution Chinese Character Generator[J]. , 1986, 1(2): 1 -14 .
[3] Sun Zhongxiu; Shang Lujun;. DMODULA:A Distributed Programming Language[J]. , 1986, 1(2): 25 -31 .
[4] Gao Qingshi; Zhang Xiang; Yang Shufan; Chen Shuqing;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[5] Min Yinghua; Han Zhide;. A Built-in Test Pattern Generator[J]. , 1986, 1(4): 62 -74 .
[6] Shi Zhongzhi;. Knowledge-Based Decision Support System[J]. , 1987, 2(1): 22 -29 .
[7] Tang Tonggao; Zhao Zhaokeng;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] Zhong Renbao; Xing Lin; Ren Zhaoyang;. An Interactive System SDI on Microcomputer[J]. , 1987, 2(1): 64 -71 .
[9] Min Yinghua;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[10] Qiao Xiangzhen;. An Efficient Parallel Algorithm for FFT[J]. , 1987, 2(3): 174 -190 .

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

 Home
Editorial Board
Author Guidelines
Subscription		 Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved