Explicit State Model Checking in the Development Process for Interlocking Software Systems – Extended Abstract –

We report on an ongoing project1 that addresses the use of explicit state model checking technology in the design of railroad interlocking systems. We discuss our modeling approach, the requirements on the use of formal methods as specified in the pertinent CENELEC standards, and the use of explicit state model checking in requirements verification and test case generation. In the context of test case generation we also illustrate the use of heuristic search strategies in model checking. I. CASE STUDY We consider the design of a generic Track Segment Oc