Safety analysis of a railway level crossing using coloured petri nets

This paper proposes an approach for safety analysis of a railway level crossing system, incorporating system topology, component function table, component state transition table and digraph in one formal model. The approach takes advantage of coloured Petri nets to model the level crossing system, and considers the system as the composition of a controller and a controlled technical process. The controller is modelled with a component-based method, while the technical process is described by a process/state-based means. Safety analysis is accomplished by investigating the reachability properties of the system model. To alleviate the state space problem of Petri nets, we employ the Petri net unfoldings to substitute reachability graphs.