Application of Petri Based Verification Approach in Safety Communication Protocol for ETCS
Linfang Cheng, Fei Wang, Xianqiong Zhao · Modern Transportation · 2013
As the performance of secure communication protocol directly affects the safety state of train in train operation control system, the performance analysis and verification is an important means to guarantee the train safety. secure communication protocol of ETCS is the subject of this paper; then performance analysis and verification are put forward based on Petri; by which model is developed by means of CPN (Colored Petri Net); then boundedness, liveness, and safety of the protocol are investigated using formal method; further, based on the model state and action, whether the protocol agrees with standard is examined. The above mentioned functions are realized by Petri including Poseidon and CPN Tools.