No Cover Image

Conference Paper/Proceeding/Abstract 270 views

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

Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, Volume: 14198, Pages: 211 - 224

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

  • Accepted Manuscript under embargo until: 27th September 2024

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