Improving Railway Safety: Human-in-the-loop Invariant Finding - Ben Lloyd-Roberts (Extended Abstracts of the 2023 CHI Conference on Human Factors in Computing Systems, 2023)
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 within the railway sector. However, many contemporary approaches frequently detect false positive safety violations that can require lengthy manual analysis by expert engineers. It hasbeen 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.In this work, we report on the use of machine learning to explore such state spaces autonomously and provide various visual aids to assist engineers in understanding and inducing invariant properties to help with verification. We conducted a focus group with an engineering team specialising in railway signalling systems, soliciting feedback on these visualisations and co-designing suggested improvements for the application domain. The results were two-fold; our visualisations allowed participants to explore invariants, but also highlighted improvements to our invariant mining approach by leveraging their domain knowledge.