We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 35 Issue 6
November  2020
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Supplements
Qian-Qian Lin, Shu-Ling Wang, Bo-Hua Zhan, Bin Gu. Modelling and Verification of Real-Time Publish and Subscribe Protocol Using UPPAAL and Simulink/Stateflow[J]. Journal of Computer Science and Technology, 2020, 35(6): 1324-1342. DOI: 10.1007/s11390-020-0537-8
Citation: Qian-Qian Lin, Shu-Ling Wang, Bo-Hua Zhan, Bin Gu. Modelling and Verification of Real-Time Publish and Subscribe Protocol Using UPPAAL and Simulink/Stateflow[J]. Journal of Computer Science and Technology, 2020, 35(6): 1324-1342. DOI: 10.1007/s11390-020-0537-8
shu

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

  • 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

Funds: 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.
More Information
  • Author Bio:

    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.

  • Corresponding author:

    Bin Gu E-mail: gubinbj@sina.com

  • Received Date: April 10, 2020
  • Revised Date: October 09, 2020
  • Published Date: November 19, 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.
    • FullText(HTML)
    • References (26)
  • [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.
    • Relative Articles

  • Related Articles

    [1]Zhao-Hui Li, Xin-Yu Feng. Verifying Contextual Refinement with Ownership Transfer[J]. Journal of Computer Science and Technology, 2021, 36(6): 1342-1366. DOI: 10.1007/s11390-021-1671-7
    [2]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. DOI: 10.1007/s11390-020-0538-7
    [3]Xu-Tao Du, Chun-Xiao Xing, Li-Zhu Zhou. Modeling and Verifying Concurrent Programs with Finite Chu Spaces[J]. Journal of Computer Science and Technology, 2010, 25(6): 1168-1183. DOI: 10.1007/s11390-010-1093-4
    [4]Dian-Xiang Xu, Omar El-Ariss, Wei-Feng Xu, Lin-Zhang Wang. Aspect-Oriented Modeling and Verification with Finite State Machines[J]. Journal of Computer Science and Technology, 2009, 24(5): 949-961.
    [5]ZHANG Yiying, ZHU Xiaoyan, ZHANG Bo. A New Speaker Verification Method with Global Speaker Model and Likelihood Score Normalization[J]. Journal of Computer Science and Technology, 2000, 15(2): 184-193.
    [6]Liu Tong, C.S.Tang. Semantic Specification and Verification of Data Flow Diagrams[J]. Journal of Computer Science and Technology, 1991, 6(1): 21-31.
    [7]Zhao Xudong, Feng Yulin. Automatic and Hierarchical Verification for Concurrent Systems[J]. Journal of Computer Science and Technology, 1990, 5(3): 241-249.
    [8]Sun Yongqiang. Verification of Systolic Array:An FP Functional Approach[J]. Journal of Computer Science and Technology, 1988, 3(2): 81-101.
    [9]Lu Qi, Zhang Fubo, Qian Jiahua. Program Slicing:Its Improved Algorithm and Application in Verification[J]. Journal of Computer Science and Technology, 1988, 3(1): 29-39.
    [10]Gong Zhenhe. On Conceptual Model Specification and Verification[J]. Journal of Computer Science and Technology, 1987, 2(1): 35-50.
    • Supplements (2)

  • Others

  • Cited by

    Periodical cited type(11)

    1. Wenbo Zhou, Yujiao Zhao, Ye Zhang, et al. A comprehensive survey of UPPAAL‐assisted formal modeling and verification. Software: Practice and Experience, 2025, 55(2): 272. DOI:10.1002/spe.3372
    2. Samir Tigane, Fayçal Guerrouf, Nadia Hamani, et al. Dynamic Timed Automata for Reconfigurable System Modeling and Verification. Axioms, 2023, 12(3): 230. DOI:10.3390/axioms12030230
    3. Ran Li, Jiaqi Yin, Huibiao Zhu, et al. Verification of RabbitMQ with Kerberos Using Timed Automata. Mobile Networks and Applications, 2022, 27(5): 2049. DOI:10.1007/s11036-022-01986-8
    4. Panhua Guo, Bohua Zhan, Xiong Xu, et al. Translating a large subset of stateflow to hybrid CSP with code optimization. Journal of Systems Architecture, 2022, 130: 102665. DOI:10.1016/j.sysarc.2022.102665
    5. Panhua Guo, Bohua Zhan, Xiong Xu, et al. Dependable Software Engineering. Theories, Tools, and Applications. Lecture Notes in Computer Science, DOI:10.1007/978-3-030-91265-9_1
    6. Peter Backeman, Cristina Seceleanu. Rebeca for Actor Analysis in Action. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-85134-6_13
    7. Alaa A. Ali, Eman A. Abdallah, Mirna Kostandy, et al. Real-Time Control of a Rescue Drone for Efficient Firefighting Operations: Embedded Systems and StateFlow Integration. 2023 2nd International Conference on Smart Cities 4.0, DOI:10.1109/SmartCities4.056956.2023.10525233
    8. Xiao-Ying Liu, Sheng-Rong Zou, Xue Geng, et al. Conversion of Timing Diagram to Event-B. 2023 8th International Conference on Computational Intelligence and Applications (ICCIA), DOI:10.1109/ICCIA59741.2023.00021
    9. Rabia Arslan, Mehmet Akşit. Management and Engineering of Critical Infrastructures. DOI:10.1016/B978-0-323-99330-2.00008-8
    10. Jiaqi Yin, Huibiao Zhu, Yuan Fei, et al. Formal Modelling and Verification of the RTPS Behavior Module. 2021 International Symposium on Theoretical Aspects of Software Engineering (TASE), DOI:10.1109/TASE52547.2021.00028
    11. Guoyu Zhang, Zijian Zhu. The Impact of the Distance Sensors Orientation on the Obstacle Avoidance Ability of the Robot. 2022 International Conference on Machine Learning and Intelligent Systems Engineering (MLISE), DOI:10.1109/MLISE57402.2022.00018

    Other cited types(0)

Catalog

    Get Citation
    PDF
    XML
    Read Online
    Article views (81) PDF downloads (0) Cited by(11)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    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

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return