Hierarchical Model Checking Method of Safety Communication Protocol Specification

被引：0
|
作者：
Zhang Y. [1 ]
Yang L. [2 ]
Zeng X. [3 ]
Sun W. [1 ]
Liu Q. [1 ]
机构：
[1] Transportation & Economics Research Institute, China Academy of Railway Sciences Corporation Limited, Beijing
[2] Railway Science & Technology Research & Development Center, China Academy of Railway Sciences Corporation Limited, Beijing
[3] Liuzhou Station, China Railway Nanning Group Co., Ltd., Liuzhou
来源：
Zhongguo Tiedao Kexue/China Railway Science | 2021年 / 42卷 / 06期
关键词：
Colored petri net; IAN; Model checking; Protocol specification verification; Safety communication protocol; Train control system;
D O I：
10.3969/j.issn.1001-4632.2021.06.17
中图分类号：
学科分类号：
摘要：
In order to control the state-space size of the model of complex safety communication protocol specification reasonably and to discover the deadlocks, livelocks and property defects of the protocol specification clearly and completely, a hierarchical modeling and verification method according to the intrinsic layers of protocol is proposed. The tasked upper and lower layers are deeply extracted by using the Interface Automata Network (IAN) to obtain the abstract formalized model for describing the protocol specification with three layers. The built IAN model is transformed to the Color Petri Net (CPN) model using the defined transfer rules from the formalized IAN model to CPN model. The method is given to validate the two kinds of properties of existential consistency and forward mandatory consistency, which are described in the extension language ASK-CTL by using the model checking tool CPN Tools. The safety function module specification of the safety communication protocol of the train control system is selected for case study. The results show that the proposed hierarchical model checking method can control the size of the model state-space within the required space. There is no deadlock or livelock in the safety functional module specification of safety communication protocol, which indicates that the safety function module process is designed properly. However, there are such problems as unsuccessful in the connection establishment process of safety function module, unable-transmission of high priority data and the disconnection of train-ground communication. Therefore, the application layer of train control system should have the response processing for failure in connection function and the protection function of fault-oriented safety. © 2021, Editorial Department of China Railway Science. All right reserved.
引用
收藏
页码：162 / 170
页数：8
相关论文
共 18 条
  • [1] CHEN Lijie, HUANG Yinxia, GAO Ying, Et al., Method of Formulating Rule for Performance Evaluation of Safety Communication Protocol in Wireless Train Control System, China Railway Science, 39, 5, pp. 119-126, (2018)
  • [2] ZHANG Yadong, WANG Shuo, LI Ya, Et al., Hazard Analysis and Simulation Verification Method of Train Control Operation Scenarios Based on STPA and Multi-Agent, China Railway Science, 42, 1, pp. 147-155, (2021)
  • [3] ZHANG Yan, TANG Tao, MA Lianchuan, Et al., Modeling and Simulation of the Security Communication Protocol Based on the Switched Ethernet, Journal of the China Railway Society, 32, 3, pp. 43-48, (2010)
  • [4] WANG Kaifeng, ZHANG Qi, LIU Chang, Et al., Software-Defined Railway Wireless Communication Network, Journal of Tsinghua University: Science and Technology, 59, 2, pp. 142-147, (2019)
  • [5] WANG Yang, WEI Jun, WANG Zhenyu, Model Checking Distributed Control Systems Based on Software Architecture, Journal of Software, 15, 6, pp. 823-833, (2004)
  • [6] SCHAFER T, KNAPP A, MERZ S., Model Checking UML State Machines and Collaborations, Electronic Notes in Theoretical Computer Science, 55, 3, pp. 357-369, (2001)
  • [7] MEDVIDOVIC N, ROSENBLUM D S, REDMILES D F, Et al., Modeling Software Architectures in the Unified Modeling Language, ACM Transactions on Software Engineering and Methodology, 11, 1, pp. 2-57, (2002)
  • [8] OUZZIF M, ERRADI M, MOUNTASSIR H., Description of a Teleconferencing Floor Control Protocol and Its Implementation, Engineering Applications of Artificial Intelligence, 21, 3, pp. 430-441, (2008)
  • [9] DE ALFARO L, HENZINGER T A., Interface Automata, Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering-ESEC/FSE-9, pp. 109-120, (2001)
  • [10] HU Jun, YU Xiaofeng, ZHANG Yan, Et al., Checking Component-Based Designs for Scenario-Based Specifications, Chinese Journal of Computers, 29, 4, pp. 4513-4525, (2006)
12