No Cover Image

E-Thesis 66 views 36 downloads

Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification / Victor Cai

Swansea University Author: Victor Cai

Abstract

The introduction of modern signalling and control systems on the railway requires that theinfrastructure topology data be verified against a number of design constraints to ensuresafety and correctness. At [REDACTED], a software toolchain has been developed toautomate this verification process, base...

Full description

Published: Swansea University, Wales, UK 2024
Institution: Swansea University
Degree level: Master of Research
Degree name: MSc by Research
Supervisor: Roggenbach, M. and Seisenberger, M.
URI: https://cronfa.swan.ac.uk/Record/cronfa68765
first_indexed 2025-01-30T13:08:14Z
last_indexed 2025-01-30T20:25:50Z
id cronfa68765
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2025-01-30T13:08:12.0618675</datestamp><bib-version>v2</bib-version><id>68765</id><entry>2025-01-30</entry><title>Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification</title><swanseaauthors><author><sid>01a2fe6ff8f8b39b597d9ff34d49d28f</sid><firstname>Victor</firstname><surname>Cai</surname><name>Victor Cai</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-01-30</date><deptcode>MACS</deptcode><abstract>The introduction of modern signalling and control systems on the railway requires that theinfrastructure topology data be verified against a number of design constraints to ensuresafety and correctness. At [REDACTED], a software toolchain has been developed toautomate this verification process, based on a formal proof tool and its language. In this thesis,we present an enhancement to this toolchain introducing the functionality to graphicallydisplay counterexamples. The requirements for this extension is established through userengagement in the form of a focus group study, and its implementation is carried out acrossseveral industrial-sized software projects. The work involves human-computer interactiondesign, formal methods, and the development of data formats as well as programming.</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea University, Wales, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>Theoretical Computer Science, Formal Methods, Railway Verification, CounterexampleVisualisation, Domain-Specific Visualisation, Software Engineering, Railway Signalling,Railway Control Systems, European Train Control System (ETCS), European RailTraffic Management System (ERTMS), Human-Computer Interaction</keywords><publishedDay>6</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-11-06</publishedDate><doi/><url/><notes>A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information</notes><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><supervisor>Roggenbach, M. and Seisenberger, M.</supervisor><degreelevel>Master of Research</degreelevel><degreename>MSc by Research</degreename><degreesponsorsfunders>Siemens Mobility Limited</degreesponsorsfunders><apcterm/><funders>Siemens Mobility Limited</funders><projectreference/><lastEdited>2025-01-30T13:08:12.0618675</lastEdited><Created>2025-01-30T12:59:47.6239463</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>Victor</firstname><surname>Cai</surname><order>1</order></author></authors><documents><document><filename>68765__33438__4e2b29fc39ff43df9ce8bad9d6ecf40b.pdf</filename><originalFilename>2024_Cai_V.final.68765.pdf</originalFilename><uploaded>2025-01-30T13:06:37.0975959</uploaded><type>Output</type><contentLength>5932463</contentLength><contentType>application/pdf</contentType><version>E-Thesis &#x2013; open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The Author, Victor Cai, 2024</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2025-01-30T13:08:12.0618675 v2 68765 2025-01-30 Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification 01a2fe6ff8f8b39b597d9ff34d49d28f Victor Cai Victor Cai true false 2025-01-30 MACS The introduction of modern signalling and control systems on the railway requires that theinfrastructure topology data be verified against a number of design constraints to ensuresafety and correctness. At [REDACTED], a software toolchain has been developed toautomate this verification process, based on a formal proof tool and its language. In this thesis,we present an enhancement to this toolchain introducing the functionality to graphicallydisplay counterexamples. The requirements for this extension is established through userengagement in the form of a focus group study, and its implementation is carried out acrossseveral industrial-sized software projects. The work involves human-computer interactiondesign, formal methods, and the development of data formats as well as programming. E-Thesis Swansea University, Wales, UK Theoretical Computer Science, Formal Methods, Railway Verification, CounterexampleVisualisation, Domain-Specific Visualisation, Software Engineering, Railway Signalling,Railway Control Systems, European Train Control System (ETCS), European RailTraffic Management System (ERTMS), Human-Computer Interaction 6 11 2024 2024-11-06 A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University Roggenbach, M. and Seisenberger, M. Master of Research MSc by Research Siemens Mobility Limited Siemens Mobility Limited 2025-01-30T13:08:12.0618675 2025-01-30T12:59:47.6239463 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Victor Cai 1 68765__33438__4e2b29fc39ff43df9ce8bad9d6ecf40b.pdf 2024_Cai_V.final.68765.pdf 2025-01-30T13:06:37.0975959 Output 5932463 application/pdf E-Thesis – open access true Copyright: The Author, Victor Cai, 2024 true eng
title Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification
spellingShingle Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification
Victor Cai
title_short Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification
title_full Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification
title_fullStr Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification
title_full_unstemmed Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification
title_sort Show Me How It's Wrong: Counterexample Visualisation in Static Railway Verification
author_id_str_mv 01a2fe6ff8f8b39b597d9ff34d49d28f
author_id_fullname_str_mv 01a2fe6ff8f8b39b597d9ff34d49d28f_***_Victor Cai
author Victor Cai
author2 Victor Cai
format E-Thesis
publishDate 2024
institution Swansea University
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 The introduction of modern signalling and control systems on the railway requires that theinfrastructure topology data be verified against a number of design constraints to ensuresafety and correctness. At [REDACTED], a software toolchain has been developed toautomate this verification process, based on a formal proof tool and its language. In this thesis,we present an enhancement to this toolchain introducing the functionality to graphicallydisplay counterexamples. The requirements for this extension is established through userengagement in the form of a focus group study, and its implementation is carried out acrossseveral industrial-sized software projects. The work involves human-computer interactiondesign, formal methods, and the development of data formats as well as programming.
published_date 2024-11-06T08:23:26Z
_version_ 1829996023277158400
score 11.058331

Similar Items