Conference Paper/Proceeding/Abstract 1284 views
Defining and model checking abstractions of complex railway models using CSP||B
Haifa Verification Conference 2012
Swansea University Author: Faron Moller
Abstract
The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model c...
Published in: | Haifa Verification Conference 2012 |
---|---|
Published: |
Berlin Heidelberg
Springer Verlag
2013
|
Online Access: |
http://www.cs.swan.ac.uk/~csfm/hvc12.pdf |
URI: | https://cronfa.swan.ac.uk/Record/cronfa13711 |
first_indexed |
2013-07-23T12:10:44Z |
---|---|
last_indexed |
2018-02-09T04:44:35Z |
id |
cronfa13711 |
recordtype |
SURis |
fullrecord |
<?xml version="1.0"?><rfc1807><datestamp>2015-07-01T09:19:12.8969989</datestamp><bib-version>v2</bib-version><id>13711</id><entry>2012-12-16</entry><title>Defining and model checking abstractions of complex railway models using CSP||B</title><swanseaauthors><author><sid>bf25e0b52fe7c11c473cc48d306073f7</sid><ORCID>0000-0001-9535-8053</ORCID><firstname>Faron</firstname><surname>Moller</surname><name>Faron Moller</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-12-16</date><deptcode>MACS</deptcode><abstract>The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model checked to ensure the safety properties, which must also hold in the corresponding concrete track plan, so that we will never need to model check the concrete track plan directly. We also identify the minimal number of trains that needs to be considered as part of the model checking, and we demonstrate the practicality of the approach on various scenarios.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Haifa Verification Conference 2012</journal><publisher>Springer Verlag</publisher><placeOfPublication>Berlin Heidelberg</placeOfPublication><issnPrint/><issnElectronic/><keywords>formal methods, model checking, railway verification</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2013</publishedYear><publishedDate>2013-12-31</publishedDate><doi/><url>http://www.cs.swan.ac.uk/~csfm/hvc12.pdf</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2015-07-01T09:19:12.8969989</lastEdited><Created>2012-12-16T19:19:12.8248727</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>Faron</firstname><surname>Moller</surname><orcid>0000-0001-9535-8053</orcid><order>1</order></author><author><firstname>Hoang Nga</firstname><surname>Nguyen</surname><order>2</order></author><author><firstname>Markus</firstname><surname>Roggenbach</surname><order>3</order></author><author><firstname>Steve</firstname><surname>Schneider</surname><order>4</order></author><author><firstname>Helen</firstname><surname>Treharne</surname><order>5</order></author></authors><documents/><OutputDurs/></rfc1807> |
spelling |
2015-07-01T09:19:12.8969989 v2 13711 2012-12-16 Defining and model checking abstractions of complex railway models using CSP||B bf25e0b52fe7c11c473cc48d306073f7 0000-0001-9535-8053 Faron Moller Faron Moller true false 2012-12-16 MACS The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model checked to ensure the safety properties, which must also hold in the corresponding concrete track plan, so that we will never need to model check the concrete track plan directly. We also identify the minimal number of trains that needs to be considered as part of the model checking, and we demonstrate the practicality of the approach on various scenarios. Conference Paper/Proceeding/Abstract Haifa Verification Conference 2012 Springer Verlag Berlin Heidelberg formal methods, model checking, railway verification 31 12 2013 2013-12-31 http://www.cs.swan.ac.uk/~csfm/hvc12.pdf COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2015-07-01T09:19:12.8969989 2012-12-16T19:19:12.8248727 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Faron Moller 0000-0001-9535-8053 1 Hoang Nga Nguyen 2 Markus Roggenbach 3 Steve Schneider 4 Helen Treharne 5 |
title |
Defining and model checking abstractions of complex railway models using CSP||B |
spellingShingle |
Defining and model checking abstractions of complex railway models using CSP||B Faron Moller |
title_short |
Defining and model checking abstractions of complex railway models using CSP||B |
title_full |
Defining and model checking abstractions of complex railway models using CSP||B |
title_fullStr |
Defining and model checking abstractions of complex railway models using CSP||B |
title_full_unstemmed |
Defining and model checking abstractions of complex railway models using CSP||B |
title_sort |
Defining and model checking abstractions of complex railway models using CSP||B |
author_id_str_mv |
bf25e0b52fe7c11c473cc48d306073f7 |
author_id_fullname_str_mv |
bf25e0b52fe7c11c473cc48d306073f7_***_Faron Moller |
author |
Faron Moller |
author2 |
Faron Moller Hoang Nga Nguyen Markus Roggenbach Steve Schneider Helen Treharne |
format |
Conference Paper/Proceeding/Abstract |
container_title |
Haifa Verification Conference 2012 |
publishDate |
2013 |
institution |
Swansea University |
publisher |
Springer Verlag |
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://www.cs.swan.ac.uk/~csfm/hvc12.pdf |
document_store_str |
0 |
active_str |
0 |
description |
The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model checked to ensure the safety properties, which must also hold in the corresponding concrete track plan, so that we will never need to model check the concrete track plan directly. We also identify the minimal number of trains that needs to be considered as part of the model checking, and we demonstrate the practicality of the approach on various scenarios. |
published_date |
2013-12-31T03:25:40Z |
_version_ |
1822461515570085888 |
score |
11.048604 |