Layout Validation Using Graph Grammar and Generation of Yard Specific Safety Properties for Railway Interlocking Verification

In railway electronic interlocking system, the automatic signalling equipment is programmed with the configuration data derived manually from the yard layout. This step is prone to human errors and any error can be a severe threat to signalling safety. The yard-layout data and the configured system both need to be verified to satisfy the desired safety requirements. The configured signalling system is needed to be verified against those relevant safety properties before deploying. Accordingly, the contributions in this paper include, (a) validation of input in terms of yard-layout data against some spatial properties (b) generation of yard-specific properties from the validated layout data for interlocking system verification. The work described in this paper is applied for signalling rules followed by Indian Railways. To capture the actual environment, a set of complex properties including properties involving timers is considered. Higher level safety properties such as no-collision and no-derailment are also considered for enumeration.