No Cover Image

Conference Paper/Proceeding/Abstract 1082 views

Defining and model checking abstractions of complex railway models using CSP||B

Faron Moller Orcid Logo, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, Helen Treharne

Haifa Verification Conference 2012

Swansea University Author: Faron Moller Orcid Logo

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

Full description

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
Tags: Add Tag
No Tags, Be the first to tag this record!
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>SCS</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>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</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 SCS 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 Computer Science COLLEGE CODE SCS 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:15:40Z
_version_ 1763750277650841600
score 10.999161

Similar Items