Verification of solid state interlocking programs

Abstract. We report on the inclusion of a formal method into an in-dustrial design process. Concretely, we suggest carrying out a verification step in railway interlocking design between programming the interlock-ing and testing this program. Safety still relies on testing, but the burden of guaranteeing completeness and correctness of the validation is in this way greatly reduced. We present a complete methodology for carrying out this verification step in the case of ladder logic programs and give re-sults for real world railway interlockings. As this verification step reduces costs for testing, Invensys Rail is working to include such a verification step into their design process of solid state interlockings.