Safety Invariant Engineering for Interlocking Verification

Safety Invariant Engineering for Interlocking Verification

연구 분야: Analysis

학회: International Conference on Computer Safety, Reliability, and Security

The paper discusses our work on formal static verification of interlocking functional safety via inductive safety invariants. The comprehensiveness and fidelity of verification are determined by the scope and adequacy of the safety invariants in question. This becomes a central issue when verification is done in industrial settings, as engineers need to know exactly how the invariants are related to the safety standards, which invariants are verified and, in case of violations, in what specific ways they fail. In our work, formal verification relies on the SafeCap toolset which supports fully automated verification by mathematical proof. The development of safety invariants is a critical part of its design. The main contribution of the paper is the definition of a systematic engineering method for this development and its core stages: invariant elicitation, false positive reduction, reporting all possible violations, and regression testing. We explain how these stages are carried out and which, if any, changes in the toolset they require. The method has been continuously and successfully used in the recent improvements and the extensions of SafeCap while the technology has been applied in numerous live signalling projects.