Design And Verification Of Safety Communication Protocol In STP System Based On Colored Petri Nets

The Shunting Train Protection system is used to assure the safety and improve the efficiency of the locomotive trains in the station.Recently,with the increasing and the complexity of the workload during the in-station transfer operation,the security requirements for STP system are also improving.According to this,the paper proposes a safety communication protocol for STP system and verifies it based on formal Petri models.The results show that the designed STP safety communication protocol meets the security functions of En50159-2010,which can resist the transmission threats in the channel.The main research contents are as follows:(1)Analyzing safety communication requirements of STP system.According to the functional structure of STP?existing communication modes between on-board equipment and ground equipment? safety requirements in En50159-2010,the paper analysis the overall requirements of STP safety communication protocol.(2)Designing safety communication protocol by using natural language.STP safety communication protocol innovates basing on EuroRadio and RSSP-?,which has hierarchical architecture and adopts different protective measures to resist the transmission threats in the channel.(3)Building formal models of STP safety communication protocol by using colored Petri Nets.According to the structure of STP communication system and the hierarchical structures of protocol,the paper first build basic interface models and then build protection mechanism models of the protocol,which is based on Petri Nets.(4)Formal verification and performance analysis of the protocol.The paper uses ASK-CTL model checking combining with state space analysis and performance simulation to verify the safety communication protocol.By using such three methods to verify the protocol can make the verification much more comprehensive.This paper first introduces ASK-CTL model checking on the verification of communication protocol,which make up the deficiency of the verification that only based on state space analysis and performance simulation.