No Cover Image

Conference Paper/Proceeding/Abstract 374 views 67 downloads

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

Ben Lloyd-Roberts, Phillip James, Mike Edwards Orcid Logo, Simon Robinson Orcid Logo, Phillip James Orcid Logo, Thomas Werner

Extended Abstracts of the 2023 CHI Conference on Human Factors in Computing Systems

Swansea University Authors: Ben Lloyd-Roberts, Phillip James, Mike Edwards Orcid Logo, Simon Robinson Orcid Logo, Phillip James Orcid Logo

DOI (Published version): 10.1145/3544549.3573853

Abstract

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 corr...

Full description

Published in: Extended Abstracts of the 2023 CHI Conference on Human Factors in Computing Systems
ISBN: 978-1-4503-9422-2
Published: New York, NY, USA ACM 2023
Online Access: http://dx.doi.org/10.1145/3544549.3573853
URI: https://cronfa.swan.ac.uk/Record/cronfa62272
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: 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.
Keywords: Formal verification, machine learning, data visualisation
College: Faculty of Science and Engineering