Testing of a Railway RBC in ERTMS Level 2 using Formal Methods

WALTERS, ALED

doi:https://doi.org/

E-Thesis 332 views 313 downloads

Testing of a Railway RBC in ERTMS Level 2 using Formal Methods / ALED WALTERS

Swansea University Author: ALED WALTERS

PDF | E-Thesis – open access

Copyright: The Author, Aled Rhys Walters, 2024
Download (3.96MB)

Abstract

Railway technology has been evolving over the last few decades, with current technologies oﬀering many possible advancements. With a solid foundation of knowledge the railway system has much potential, as seen with the European Rail Traﬃc Management System which oﬀers a uniﬁed operation across many...

Full description

Published:	Swansea, Wales, UK 2024
Institution:	Swansea University
Degree level:	Master of Philosophy
Degree name:	M.Phil
Supervisor:	Roggenbach, M., and Seisenberger, M.
URI:	https://cronfa.swan.ac.uk/Record/cronfa68773

first_indexed	2025-01-31T14:25:39Z
last_indexed	2025-05-10T08:16:13Z
id	cronfa68773
recordtype	RisThesis
fullrecord	<?xml version="1.0"?><rfc1807><datestamp>2025-05-09T14:29:58.7166258</datestamp><bib-version>v2</bib-version><id>68773</id><entry>2025-01-31</entry><title>Testing of a Railway RBC in ERTMS Level 2 using Formal Methods</title><swanseaauthors><author><sid>f6294bb6fc12ae9f1a7072b1f7b8e9a8</sid><firstname>ALED</firstname><surname>WALTERS</surname><name>ALED WALTERS</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-01-31</date><abstract>Railway technology has been evolving over the last few decades, with current technologies oﬀering many possible advancements. With a solid foundation of knowledge the railway system has much potential, as seen with the European Rail Traﬃc Management System which oﬀers a uniﬁed operation across many countries. However with some developmental freedom, the integration of new technologies with well understood systems can provide issues. With the addition of Radio Block Centres to existing Interlockings, Controllers, Train and Trackside equipment, there is great potential for many new positives to an old industry. Safety is a key issue in adding any new aspect to a system that still has risks, be it down to human or computer errors. The testing of RBCs remains crucial to keeping railways safe and eﬃcient, however that testing can be costly and time consuming. By modelling with formal methods, we suggest that an auxiliary testing approach could be beneﬁcial. By modelling and verifying an abstracted version of these new systems, errors could be caught in a more time- and cost-eﬀective manner, allowing for the most rigorous testing to give maximum impact. Building on work by James et al. and Berger et al., and a partnership with Siemens Rail Automation we examine the suitability of existing models in relation to current industrial testing methods, then proceed to develop our own approach in CSP\|\|B using a discrete-eventmodelling approach. Our model is then veriﬁed for collision-free safety and simulated, then compared with results from industrial simulations.</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea, Wales, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>ERTMS, European Rail Traffic Management System, Railway, Testing, Verification, RBC, Radio Block Centre</keywords><publishedDay>16</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-11-16</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><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Roggenbach, M., and Seisenberger, M.</supervisor><degreelevel>Master of Philosophy</degreelevel><degreename>M.Phil</degreename><degreesponsorsfunders>ICASE doctoral studentship funding, Siemens Rails Automation</degreesponsorsfunders><apcterm/><funders>ICASE doctoral studentship funding, Siemens Rails Automation</funders><projectreference/><lastEdited>2025-05-09T14:29:58.7166258</lastEdited><Created>2025-01-31T14:00:27.5928270</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>ALED</firstname><surname>WALTERS</surname><order>1</order></author></authors><documents><document><filename>68773__33466__a88e6ef3f5744cb0b09a9b32afd51588.pdf</filename><originalFilename>2024_Walters_A.final.68773.pdf</originalFilename><uploaded>2025-01-31T14:23:26.5746990</uploaded><type>Output</type><contentLength>4157477</contentLength><contentType>application/pdf</contentType><version>E-Thesis – open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The Author, Aled Rhys Walters, 2024</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling	2025-05-09T14:29:58.7166258 v2 68773 2025-01-31 Testing of a Railway RBC in ERTMS Level 2 using Formal Methods f6294bb6fc12ae9f1a7072b1f7b8e9a8 ALED WALTERS ALED WALTERS true false 2025-01-31 Railway technology has been evolving over the last few decades, with current technologies oﬀering many possible advancements. With a solid foundation of knowledge the railway system has much potential, as seen with the European Rail Traﬃc Management System which oﬀers a uniﬁed operation across many countries. However with some developmental freedom, the integration of new technologies with well understood systems can provide issues. With the addition of Radio Block Centres to existing Interlockings, Controllers, Train and Trackside equipment, there is great potential for many new positives to an old industry. Safety is a key issue in adding any new aspect to a system that still has risks, be it down to human or computer errors. The testing of RBCs remains crucial to keeping railways safe and eﬃcient, however that testing can be costly and time consuming. By modelling with formal methods, we suggest that an auxiliary testing approach could be beneﬁcial. By modelling and verifying an abstracted version of these new systems, errors could be caught in a more time- and cost-eﬀective manner, allowing for the most rigorous testing to give maximum impact. Building on work by James et al. and Berger et al., and a partnership with Siemens Rail Automation we examine the suitability of existing models in relation to current industrial testing methods, then proceed to develop our own approach in CSP\|\|B using a discrete-eventmodelling approach. Our model is then veriﬁed for collision-free safety and simulated, then compared with results from industrial simulations. E-Thesis Swansea, Wales, UK ERTMS, European Rail Traffic Management System, Railway, Testing, Verification, RBC, Radio Block Centre 16 11 2024 2024-11-16 A selection of content is redacted or is partially redacted from this thesis to protect sensitive and personal information. COLLEGE NANME COLLEGE CODE Swansea University Roggenbach, M., and Seisenberger, M. Master of Philosophy M.Phil ICASE doctoral studentship funding, Siemens Rails Automation ICASE doctoral studentship funding, Siemens Rails Automation 2025-05-09T14:29:58.7166258 2025-01-31T14:00:27.5928270 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science ALED WALTERS 1 68773__33466__a88e6ef3f5744cb0b09a9b32afd51588.pdf 2024_Walters_A.final.68773.pdf 2025-01-31T14:23:26.5746990 Output 4157477 application/pdf E-Thesis – open access true Copyright: The Author, Aled Rhys Walters, 2024 true eng
title	Testing of a Railway RBC in ERTMS Level 2 using Formal Methods
spellingShingle	Testing of a Railway RBC in ERTMS Level 2 using Formal Methods ALED WALTERS
title_short	Testing of a Railway RBC in ERTMS Level 2 using Formal Methods
title_full	Testing of a Railway RBC in ERTMS Level 2 using Formal Methods
title_fullStr	Testing of a Railway RBC in ERTMS Level 2 using Formal Methods
title_full_unstemmed	Testing of a Railway RBC in ERTMS Level 2 using Formal Methods
title_sort	Testing of a Railway RBC in ERTMS Level 2 using Formal Methods
author_id_str_mv	f6294bb6fc12ae9f1a7072b1f7b8e9a8
author_id_fullname_str_mv	f6294bb6fc12ae9f1a7072b1f7b8e9a8_***_ALED WALTERS
author	ALED WALTERS
author2	ALED WALTERS
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	Railway technology has been evolving over the last few decades, with current technologies oﬀering many possible advancements. With a solid foundation of knowledge the railway system has much potential, as seen with the European Rail Traﬃc Management System which oﬀers a uniﬁed operation across many countries. However with some developmental freedom, the integration of new technologies with well understood systems can provide issues. With the addition of Radio Block Centres to existing Interlockings, Controllers, Train and Trackside equipment, there is great potential for many new positives to an old industry. Safety is a key issue in adding any new aspect to a system that still has risks, be it down to human or computer errors. The testing of RBCs remains crucial to keeping railways safe and eﬃcient, however that testing can be costly and time consuming. By modelling with formal methods, we suggest that an auxiliary testing approach could be beneﬁcial. By modelling and verifying an abstracted version of these new systems, errors could be caught in a more time- and cost-eﬀective manner, allowing for the most rigorous testing to give maximum impact. Building on work by James et al. and Berger et al., and a partnership with Siemens Rail Automation we examine the suitability of existing models in relation to current industrial testing methods, then proceed to develop our own approach in CSP\|\|B using a discrete-eventmodelling approach. Our model is then veriﬁed for collision-free safety and simulated, then compared with results from industrial simulations.
published_date	2024-11-16T05:20:37Z
_version_	1851731567866544128
score	11.090464

Testing of a Railway RBC in ERTMS Level 2 using Formal Methods / ALED WALTERS

Similar Items