No Cover Image

Book chapter 474 views 20 downloads

A Tool-Chain for the Verification of Geographic Scheme Data

Madhusree Banerjee, Victor Cai, Sunitha Lakshmanappa, Andrew Lawrence, Markus Roggenbach Orcid Logo, Monika Seisenberger Orcid Logo, Thomas Werner

Lecture Notes in Computer Science, Volume: 14198, Pages: 211 - 224

Swansea University Authors: Markus Roggenbach Orcid Logo, Monika Seisenberger Orcid Logo

Check full text

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...

Full description

Published in: Lecture Notes in Computer Science
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
first_indexed 2023-07-10T13:48:12Z
last_indexed 2024-11-25T14:12:59Z
id cronfa63851
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2024-10-02T16:47:34.7018771</datestamp><bib-version>v2</bib-version><id>63851</id><entry>2023-07-10</entry><title>A Tool-Chain for&#xA0;the&#xA0;Verification of&#xA0;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>MACS</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>Book chapter</type><journal>Lecture Notes in Computer Science</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/><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>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2024-10-02T16:47:34.7018771</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>63851__28070__f3f702e9c069490c949fae4fbca08450.pdf</filename><originalFilename>63851.pdf</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><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2024-10-02T16:47:34.7018771 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 MACS 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. Book chapter Lecture Notes in Computer Science 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 Conference series: RSSRail: International Conference on Reliability, Safety, and Security of Railway Systems. Lecture Notes in Computer Science (LNCS, volume 14198) COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2024-10-02T16:47:34.7018771 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 63851__28070__f3f702e9c069490c949fae4fbca08450.pdf 63851.pdf 2023-07-10T14:48:11.2352454 Output 641661 application/pdf Accepted Manuscript true 2024-09-27T00:00:00.0000000 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 Book chapter
container_title Lecture Notes in Computer Science
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
document_store_str 1
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-27T05:27:23Z
_version_ 1821382009764708352
score 11.04748

Similar Items