Conference Paper/Proceeding/Abstract 49 views
Improving Railway Safety: Human-in-the-loop Invariant Finding
Ben Lloyd-Roberts,
Phillip James 
,
Mike Edwards ,
Thomas Werner,
Simon Robinson
,
Mike Edwards ,
Thomas Werner,
Simon Robinson
CHI 2023 Extend Abstracts
Swansea University Authors:
Ben Lloyd-Roberts, Phillip James , Mike Edwards , Simon Robinson
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...
| Published in: | CHI 2023 Extend Abstracts |
|---|---|
| Published: |
ACM
|
| 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 |