Specification and verification of safety properties along a crossing region in a railway network control

Modeling the controller of the railway network, having resource sharing based on mutual exclusion constraints, is an important problem. This paper firstly addresses the specification of safety properties for the model of a complex railway crossing. The operations, i.e., occupied, free and block, are formalized to describe the safety properties along railway crossing. Second, to develop the control model of the crossing system we construct the subnet representing the train flow along the tracks in the crossing region and the set of monitors or supervisors are also modeled as subnets. Arc-constant colored Petri net (ac-CPN) is used to construct the train flow subnet while the monitors are modeled using the place/transition-net. Arc-constant colored Petri net enforces the specification of not to shift the train from a track to another one. Bottom-up approach is adopted to model the control for railway crossing as a synchronous synthesis of the subnets is applied to build the final model. Finally, to verify the safety properties in the developed controller, the coverability tree method is used for the analysis of the final model.