Automated Compositional Verification of Interlocking Systems

Model checking techniques have often been applied to the verification of railway interlocking systems. However, these techniques may fail to scale to interlockings controlling large railway networks, composed by hundreds of controlled entities, due to the state space explosion problem. We have previously proposed a compositional method to reduce the size of networks to be model checked: the idea is to divide the network of the system to be verified into two sub-networks and then model check the model instances for these sub-networks instead of that for the full network. If given well-formedness conditions are satisfied by the network and the kind of division performed, it is proved that model checking safety properties of all such sub-networks guarantees safety properties of the full network. In this paper we observe that such a network division can be repeated, so that in the end, the full network has been divided into a number of sub-networks of minimal size, each being an instance of one of a limited set of "elementary networks", for which safety proofs have easily been given by model checking once for all. The paper defines a division algorithm, and shows how, applying it to some examples of different complexity, a network can be automatically decomposed into a set of elementary networks, hence proving its safety. The execution time for such a verification turns out to be a very small fraction of the time needed for a model checker to verify safety of the full network.