Verification of the safety communication protocol in train control system using colored Petri net

This paper deals with formal and simulation-based verification of the safety communication protocol in ETCS (European Train Control System). The safety communication protocol controls the establishment of safety connection between train and trackside. Because of its graphical user interface and modeling flexibility upon the changes in the system conditions, this paper proposes a composition colored petri net (CPN) representation for both the logic and the timed model. The logic of the protocol is proved to be safe by means of state space analysis: the dead markings are correct; there are no dead transitions; being fair. Further analysis results have been obtained using formal and simulation-based verification approach. The timed models for the open transmit system and the application process are created for the purpose of performance analysis of the safety communication protocol. The models describe the procedure of data transmission and processing, and also provide relevant timed and stochastic factors, as well as time delay and lost packet, which may influence the time for establishment of safety connection of the protocol. Time for establishment of safety connection of the protocol in normal state is verified by formal verification, and then time for establishment of safety connection with different probability of lost packet is simulated. After verification it is found that the time for establishment of safety connection of the safety communication protocol satisfies the safety requirements.

• Record URL:
  • https://doi.org/10.1016/j.ress.2011.12.010
• Record URL:
  • http://www.sciencedirect.com/science/article/pii/S0951832011002730
• Availability:
  • Find a library where document is available. Order URL: http://worldcat.org/issn/09518320
• Supplemental Notes:
  • Abstract reprinted with permission from Elsevier
• Authors:
  • Lijie, Chen
  • Tao, Tang
  • Xianqiong, Zhao
  • Schnieder, Eckehard
• Publication Date: 2012-4

Language

• English

Media Info

• Media Type: Print
• Features: Figures; References; Tables;
• Pagination: pp 8-18
• Serial:
  • Reliability Engineering & System Safety
  • Volume: 100
  • Issue Number: 0
  • Publisher: Elsevier
  • ISSN: 0951-8320
  • Serial URL: https://www.sciencedirect.com/journal/reliability-engineering-and-system-safety

Subject/Index Terms

• TRT Terms: Automatic train control; Automatic train protection; Control systems; Logic; Petri nets; Railroad safety
• Subject Areas: Data and Information Technology; Railroads; Safety and Human Factors;

Filing Info

• Accession Number: 01446475
• Record Type: Publication
• Files: TRIS
• Created Date: Sep 19 2012 10:19AM