Formal Methods for Validation and Test Point Prioritization in Railway Signaling Logic

The EN50128 Railway Safety Standard recommends the use of formal methods for proving the correctness of the yard-specific logic, which was developed for electronic signaling and interlocking systems. We present a tool flow, which consists of three components. The core component uses a novel method for automatically generating the relevant safety properties for a yard from its control table. The second component proves the validity of the properties on the application logic by using a new theory of invariant checking. The third component leverages the suite of formal properties to prioritize site acceptance test points. Experimental results are presented on real application data for the yards in India that are demonstrating the performance of the proposed methods.