Improving Railway Safety: Human-in-the-loop Invariant Finding

Formal methods is a field that has a long standing history within Computer Science. At its core, it involves the use of mathematical formalisms to model and reason about computer systems and programs. The application of formal methods to verify that railway signalling systems operate safely and correctly is particularly well established within academia and is now beginning to see real applications in the railway sector. However, many contemporary approaches frequently detect false positive safety violations necessitating lengthy manual analysis by expert engineers. It has been shown that such errors can be mitigated with strengthening invariants, non-trivially generated properties which hold for all reachable states, or configurations, of a program under verification.