Conference Paper/Proceeding/Abstract 270 views
A Tool-Chain for the Verification of Geographic Scheme Data
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, Volume: 14198, Pages: 211 - 224
Swansea University Authors:
Markus Roggenbach , Monika Seisenberger
DOI (Published version): 10.1007/978-3-031-43366-5_13
Abstract
The Engineering Data Preparation System (E-DPS) is a tool-chain produced by Siemens Mobility Limited for digital railway scheme design. This paper is concerned with the creation of a tool able to formally verify that the scheme plans follow the design rules required for correct European Train Contro...
Published in: | Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification |
---|---|
ISBN: | 9783031433658 9783031433665 |
ISSN: | 0302-9743 1611-3349 |
Published: |
Cham
Springer Nature Switzerland
2023
|
Online Access: |
Check full text
|
URI: | https://cronfa.swan.ac.uk/Record/cronfa63851 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
first_indexed |
2023-07-10T13:48:12Z |
---|---|
last_indexed |
2023-07-10T13:48:12Z |
id |
cronfa63851 |
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>63851</id><entry>2023-07-10</entry><title>A Tool-Chain for the Verification of Geographic Scheme Data</title><swanseaauthors><author><sid>7733869ae501442da6926fac77cd155b</sid><ORCID>0000-0002-3819-2787</ORCID><firstname>Markus</firstname><surname>Roggenbach</surname><name>Markus Roggenbach</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>d035399b2b324a63fe472ce0344653e0</sid><ORCID>0000-0002-2226-386X</ORCID><firstname>Monika</firstname><surname>Seisenberger</surname><name>Monika Seisenberger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2023-07-10</date><deptcode>SCS</deptcode><abstract>The Engineering Data Preparation System (E-DPS) is a tool-chain produced by Siemens Mobility Limited for digital railway scheme design. This paper is concerned with the creation of a tool able to formally verify that the scheme plans follow the design rules required for correct European Train Control System (ETCS) operation. The E-DPS Checker encodes the scheme plan and signalling design rules as an attributed graph and logical constraints over that graph, respectively. Logical constraints are verified by the E-DPS Checker using the satisfiability modulo theories solver Z3. This approach verifies the configuration of ETCS for a particular scheme and reduces the amount of principles testing and manual checking required. The E-DPS Checker is currently being developed to EN50128 basic integrity and has been applied to verify the correctness of a number of real-world scheme plans as part of the development process.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification</journal><volume>14198</volume><journalNumber/><paginationStart>211</paginationStart><paginationEnd>224</paginationEnd><publisher>Springer Nature Switzerland</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint>9783031433658</isbnPrint><isbnElectronic>9783031433665</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>Safety, reliability, security, railway systems, formal methods, computer systems organization, embedded and cyber-physical systems, real time systems, theory of security, architecture</keywords><publishedDay>27</publishedDay><publishedMonth>9</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-09-27</publishedDate><doi>10.1007/978-3-031-43366-5_13</doi><url>http://dx.doi.org/10.1007/978-3-031-43366-5_13</url><notes>Conference series: RSSRail: International Conference on Reliability, Safety, and Security of Railway Systems. Lecture Notes in Computer Science (LNCS, volume 14198)</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2024-04-08T14:05:46.8907253</lastEdited><Created>2023-07-10T14:32:19.4451704</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>Madhusree</firstname><surname>Banerjee</surname><order>1</order></author><author><firstname>Victor</firstname><surname>Cai</surname><order>2</order></author><author><firstname>Sunitha</firstname><surname>Lakshmanappa</surname><order>3</order></author><author><firstname>Andrew</firstname><surname>Lawrence</surname><order>4</order></author><author><firstname>Markus</firstname><surname>Roggenbach</surname><orcid>0000-0002-3819-2787</orcid><order>5</order></author><author><firstname>Monika</firstname><surname>Seisenberger</surname><orcid>0000-0002-2226-386X</orcid><order>6</order></author><author><firstname>Thomas</firstname><surname>Werner</surname><order>7</order></author></authors><documents><document><filename>Under embargo</filename><originalFilename>Under embargo</originalFilename><uploaded>2023-07-10T14:48:11.2352454</uploaded><type>Output</type><contentLength>641661</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2024-09-27T00:00:00.0000000</embargoDate><documentNotes>Accepted Manuscript Version. c The Author(s), under exclusive license to Springer Nature Switzerland AG 2023B. Milius et al. (Eds.): RSSRail 2023, LNCS 14198, pp. 211–224, 2023.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807> |
spelling |
v2 63851 2023-07-10 A Tool-Chain for the Verification of Geographic Scheme Data 7733869ae501442da6926fac77cd155b 0000-0002-3819-2787 Markus Roggenbach Markus Roggenbach true false d035399b2b324a63fe472ce0344653e0 0000-0002-2226-386X Monika Seisenberger Monika Seisenberger true false 2023-07-10 SCS The Engineering Data Preparation System (E-DPS) is a tool-chain produced by Siemens Mobility Limited for digital railway scheme design. This paper is concerned with the creation of a tool able to formally verify that the scheme plans follow the design rules required for correct European Train Control System (ETCS) operation. The E-DPS Checker encodes the scheme plan and signalling design rules as an attributed graph and logical constraints over that graph, respectively. Logical constraints are verified by the E-DPS Checker using the satisfiability modulo theories solver Z3. This approach verifies the configuration of ETCS for a particular scheme and reduces the amount of principles testing and manual checking required. The E-DPS Checker is currently being developed to EN50128 basic integrity and has been applied to verify the correctness of a number of real-world scheme plans as part of the development process. Conference Paper/Proceeding/Abstract Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification 14198 211 224 Springer Nature Switzerland Cham 9783031433658 9783031433665 0302-9743 1611-3349 Safety, reliability, security, railway systems, formal methods, computer systems organization, embedded and cyber-physical systems, real time systems, theory of security, architecture 27 9 2023 2023-09-27 10.1007/978-3-031-43366-5_13 http://dx.doi.org/10.1007/978-3-031-43366-5_13 Conference series: RSSRail: International Conference on Reliability, Safety, and Security of Railway Systems. Lecture Notes in Computer Science (LNCS, volume 14198) COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2024-04-08T14:05:46.8907253 2023-07-10T14:32:19.4451704 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Madhusree Banerjee 1 Victor Cai 2 Sunitha Lakshmanappa 3 Andrew Lawrence 4 Markus Roggenbach 0000-0002-3819-2787 5 Monika Seisenberger 0000-0002-2226-386X 6 Thomas Werner 7 Under embargo Under embargo 2023-07-10T14:48:11.2352454 Output 641661 application/pdf Accepted Manuscript true 2024-09-27T00:00:00.0000000 Accepted Manuscript Version. c The Author(s), under exclusive license to Springer Nature Switzerland AG 2023B. Milius et al. (Eds.): RSSRail 2023, LNCS 14198, pp. 211–224, 2023. true eng |
title |
A Tool-Chain for the Verification of Geographic Scheme Data |
spellingShingle |
A Tool-Chain for the Verification of Geographic Scheme Data Markus Roggenbach Monika Seisenberger |
title_short |
A Tool-Chain for the Verification of Geographic Scheme Data |
title_full |
A Tool-Chain for the Verification of Geographic Scheme Data |
title_fullStr |
A Tool-Chain for the Verification of Geographic Scheme Data |
title_full_unstemmed |
A Tool-Chain for the Verification of Geographic Scheme Data |
title_sort |
A Tool-Chain for the Verification of Geographic Scheme Data |
author_id_str_mv |
7733869ae501442da6926fac77cd155b d035399b2b324a63fe472ce0344653e0 |
author_id_fullname_str_mv |
7733869ae501442da6926fac77cd155b_***_Markus Roggenbach d035399b2b324a63fe472ce0344653e0_***_Monika Seisenberger |
author |
Markus Roggenbach Monika Seisenberger |
author2 |
Madhusree Banerjee Victor Cai Sunitha Lakshmanappa Andrew Lawrence Markus Roggenbach Monika Seisenberger Thomas Werner |
format |
Conference Paper/Proceeding/Abstract |
container_title |
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification |
container_volume |
14198 |
container_start_page |
211 |
publishDate |
2023 |
institution |
Swansea University |
isbn |
9783031433658 9783031433665 |
issn |
0302-9743 1611-3349 |
doi_str_mv |
10.1007/978-3-031-43366-5_13 |
publisher |
Springer Nature Switzerland |
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 |
url |
http://dx.doi.org/10.1007/978-3-031-43366-5_13 |
document_store_str |
0 |
active_str |
0 |
description |
The Engineering Data Preparation System (E-DPS) is a tool-chain produced by Siemens Mobility Limited for digital railway scheme design. This paper is concerned with the creation of a tool able to formally verify that the scheme plans follow the design rules required for correct European Train Control System (ETCS) operation. The E-DPS Checker encodes the scheme plan and signalling design rules as an attributed graph and logical constraints over that graph, respectively. Logical constraints are verified by the E-DPS Checker using the satisfiability modulo theories solver Z3. This approach verifies the configuration of ETCS for a particular scheme and reduces the amount of principles testing and manual checking required. The E-DPS Checker is currently being developed to EN50128 basic integrity and has been applied to verify the correctness of a number of real-world scheme plans as part of the development process. |
published_date |
2023-09-27T14:05:43Z |
_version_ |
1795771904640942080 |
score |
11.013731 |