Safety Invariant Verification that Meets Engineers' Expectations.

This industrial experience report discusses the problems we have been facing while using our formal verification technology, called SafeCap, in a substantial number of live signalling projects in UK mainline rail, and the solutions we are now developing to counter these problems. Symbolic execution and safety invariant verification are well-understood subjects and yet their application to real life high assurance systems requires going a few steps beyond the conventional practice. In engineering practice it is not sufficient to simply know that a safety property fails: one needs to know why and hence where and what exactly fails. It is also crucial to positively demonstrate that no safety failure is omitted from consideration. In this industrial report we show how to derive a list of all potential errors by transforming a safety invariant predicate using information from the constructed state transition system. The identified possible errors are verified by an automated symbolic prover, while a report generator presents findings in an engineer-friendly format to guide subsequent rework steps. The scalability and the efficiency of the proposed mechanism (which is now fully integrated in the SafeCap technology) have been demonstrated in several live signalling projects.