Configurable Interlocking Verification.

This short industrial paper discusses the challenge of precisely defining the scope of formal verification in industrial applications, to avoid both unintentional omission of verification of requirements and duplication of verification. It draws on the experience of using our formal verification technology, called SafeCap, in a substantial number of live railway signalling projects in the UK , and the solutions we are now developing. SafeCap uses safety invariants (safety properties) to formally and fully automatically verify the safety of site-specific configurations of railway interlockings using a dedicated symbolic theorem prover. The scope of this formal verification is a subset of the totality of site-specific interlocking configuration verification, which itself is a subset of the totality of signalling system verification. In the course of our work, it has also become apparent that there is a need to develop and use in practice different (often overlapping) sets of properties. There are various reasons for this: different railways use different safety standards from which the properties are developed; the standards themselves evolve; their is a need for versioning and change management of the properties during the continuous improvement of our tool. To this end, the paper puts forward the idea of defining the verification scopes (called dialects) together with a mechanism of introducing a scope as a set of verification properties which are tagged with the unique scope name. The paper uses various industrial scenarios we are facing in deploying SafeCap to demonstrate how this mechanism works in our commercial deployment.