Modelling large railway interlockings and model checking small ones

Abstract

This paper describes the results to date of a feasibility study on model checking applied to railway interlockings. Our approach, in contrast to others, targets a high-level description of interlocking systems, namely the logical view of its opera- tion. The result is a formal model that can be discussed with and validated by our industry partners and, moreover, provides a formal semantics for the notation that is used in practice. We suggest optimisations on the formal model and a decomposition technique for large railway layouts that is easy to apply. This renders our approach feasible for use in industrial practice.