Functional safety verification on railway signaling system with Colored Petri Nets

Signaling system acts very important safety role in both national railway and urban rail transportation. This paper provides a formal verification framework on functional safety desired by railway industry application. The presented work chooses Colored Petri Nets for functional modeling and verification. The modelling approaches of internal faults and undesired external influences are proposed by introducing a countering place, and the verification criteria is established based on credible hazard set. An application of this framework on Communication Based Train Control system is also presented.