Compositional Model Checking of Railway Interlocking Systems Featuring Flank Protection

Model checking techniques applied to the verification of railway interlocking systems may fail to scale. Compositional methods have been proposed to reduce the size of networks to be model checked. In this paper we extend the scope of a previously defined compositional method to systems employing flank protection, not supported in the original method because flank protection requires a coordination of distant points. The extension comprises soundness results for this new context and a decomposition strategy able to divide a network into sub-networks of minimal size.