No Cover Image

Conference Paper/Proceeding/Abstract 480 views 80 downloads

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

Ben Lloyd-Roberts, Phillip James Orcid Logo, 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 Orcid Logo, 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
URI: https://cronfa.swan.ac.uk/Record/cronfa62272
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2023-01-06T12:10:28Z
last_indexed 2023-04-15T03:21:18Z
id cronfa62272
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>62272</id><entry>2023-01-06</entry><title>Improving Railway Safety: Human-in-the-loop Invariant Finding</title><swanseaauthors><author><sid>1195fd6c5ca360e99294de541c80587f</sid><firstname>Ben</firstname><surname>Lloyd-Roberts</surname><name>Ben Lloyd-Roberts</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>fd3b15ff96c5ea91a100131abac558b6</sid><ORCID>0000-0002-4307-649X</ORCID><firstname>Phillip</firstname><surname>James</surname><name>Phillip James</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>684864a1ce01c3d774e83ed55e41770e</sid><ORCID>0000-0003-3367-969X</ORCID><firstname>Mike</firstname><surname>Edwards</surname><name>Mike Edwards</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>cb3b57a21fa4e48ec633d6ba46455e91</sid><ORCID>0000-0001-9228-006X</ORCID><firstname>Simon</firstname><surname>Robinson</surname><name>Simon Robinson</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>3ded05e11923bacd96ee3ddea58b62bd</sid><ORCID>NULL</ORCID><firstname>Phillip</firstname><surname>James</surname><name>Phillip James</name><active>true</active><ethesisStudent>true</ethesisStudent></author></swanseaauthors><date>2023-01-06</date><deptcode>MACS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Extended Abstracts of the 2023 CHI Conference on Human Factors in Computing Systems</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher>ACM</publisher><placeOfPublication>New York, NY, USA</placeOfPublication><isbnPrint/><isbnElectronic>978-1-4503-9422-2</isbnElectronic><issnPrint/><issnElectronic/><keywords>Formal verification, machine learning, data visualisation</keywords><publishedDay>19</publishedDay><publishedMonth>4</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-04-19</publishedDate><doi>10.1145/3544549.3573853</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2024-05-31T16:47:31.0913109</lastEdited><Created>2023-01-06T12:03:55.8934209</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Ben</firstname><surname>Lloyd-Roberts</surname><order>1</order></author><author><firstname>Phillip</firstname><surname>James</surname><orcid>0000-0002-4307-649X</orcid><order>2</order></author><author><firstname>Mike</firstname><surname>Edwards</surname><orcid>0000-0003-3367-969X</orcid><order>3</order></author><author><firstname>Simon</firstname><surname>Robinson</surname><orcid>0000-0001-9228-006X</orcid><order>4</order></author><author><firstname>Phillip</firstname><surname>James</surname><orcid>NULL</orcid><order>5</order></author><author><firstname>Thomas</firstname><surname>Werner</surname><order>6</order></author></authors><documents><document><filename>62272__26203__d2b8a12222464ca1bd87e1346d8923f1.pdf</filename><originalFilename>Human-in-the-loop Invariant Finding.pdf</originalFilename><uploaded>2023-01-06T12:08:20.5817867</uploaded><type>Output</type><contentLength>2238113</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2023-04-23T00:00:00.0000000</embargoDate><copyrightCorrect>false</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling v2 62272 2023-01-06 Improving Railway Safety: Human-in-the-loop Invariant Finding 1195fd6c5ca360e99294de541c80587f Ben Lloyd-Roberts Ben Lloyd-Roberts true false fd3b15ff96c5ea91a100131abac558b6 0000-0002-4307-649X Phillip James Phillip James true false 684864a1ce01c3d774e83ed55e41770e 0000-0003-3367-969X Mike Edwards Mike Edwards true false cb3b57a21fa4e48ec633d6ba46455e91 0000-0001-9228-006X Simon Robinson Simon Robinson true false 3ded05e11923bacd96ee3ddea58b62bd NULL Phillip James Phillip James true true 2023-01-06 MACS 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. Conference Paper/Proceeding/Abstract Extended Abstracts of the 2023 CHI Conference on Human Factors in Computing Systems ACM New York, NY, USA 978-1-4503-9422-2 Formal verification, machine learning, data visualisation 19 4 2023 2023-04-19 10.1145/3544549.3573853 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2024-05-31T16:47:31.0913109 2023-01-06T12:03:55.8934209 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ben Lloyd-Roberts 1 Phillip James 0000-0002-4307-649X 2 Mike Edwards 0000-0003-3367-969X 3 Simon Robinson 0000-0001-9228-006X 4 Phillip James NULL 5 Thomas Werner 6 62272__26203__d2b8a12222464ca1bd87e1346d8923f1.pdf Human-in-the-loop Invariant Finding.pdf 2023-01-06T12:08:20.5817867 Output 2238113 application/pdf Accepted Manuscript true 2023-04-23T00:00:00.0000000 false
title Improving Railway Safety: Human-in-the-loop Invariant Finding
spellingShingle Improving Railway Safety: Human-in-the-loop Invariant Finding
Ben Lloyd-Roberts
Phillip James
Mike Edwards
Simon Robinson
Phillip James
title_short Improving Railway Safety: Human-in-the-loop Invariant Finding
title_full Improving Railway Safety: Human-in-the-loop Invariant Finding
title_fullStr Improving Railway Safety: Human-in-the-loop Invariant Finding
title_full_unstemmed Improving Railway Safety: Human-in-the-loop Invariant Finding
title_sort Improving Railway Safety: Human-in-the-loop Invariant Finding
author_id_str_mv 1195fd6c5ca360e99294de541c80587f
fd3b15ff96c5ea91a100131abac558b6
684864a1ce01c3d774e83ed55e41770e
cb3b57a21fa4e48ec633d6ba46455e91
3ded05e11923bacd96ee3ddea58b62bd
author_id_fullname_str_mv 1195fd6c5ca360e99294de541c80587f_***_Ben Lloyd-Roberts
fd3b15ff96c5ea91a100131abac558b6_***_Phillip James
684864a1ce01c3d774e83ed55e41770e_***_Mike Edwards
cb3b57a21fa4e48ec633d6ba46455e91_***_Simon Robinson
3ded05e11923bacd96ee3ddea58b62bd_***_Phillip James
author Ben Lloyd-Roberts
Phillip James
Mike Edwards
Simon Robinson
Phillip James
author2 Ben Lloyd-Roberts
Phillip James
Mike Edwards
Simon Robinson
Phillip James
Thomas Werner
format Conference Paper/Proceeding/Abstract
container_title Extended Abstracts of the 2023 CHI Conference on Human Factors in Computing Systems
publishDate 2023
institution Swansea University
isbn 978-1-4503-9422-2
doi_str_mv 10.1145/3544549.3573853
publisher ACM
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description 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.
published_date 2023-04-19T16:47:29Z
_version_ 1800583721728868352
score 11.017797

Similar Items