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

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

0.00 Avg rating0 Votes
Article ID: iaor20122174
Volume: 100
Issue: 2
Start Page Number: 8
End Page Number: 18
Publication Date: Apr 2012
Journal: Reliability Engineering and System Safety
Authors: , , ,
Keywords: simulation: applications, transportation: rail, communication
Abstract:

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.

Reviews

Required fields are marked *. Your email address will not be published.