No Cover Image

Journal article 1472 views

Railway modelling in CSP||B: the double junction case study

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

Electronic Communications of the European Association for the Study of Science and Technology, Volume: n/a

Swansea University Author: Faron Moller Orcid Logo

Abstract

This paper reports on recent work in verifying railway systems through CSP||B modelling and analysis. Our motivation is to develop a modelling and verification approach accessible to railway engineers: it is vital that they can validate the models and verification conditions, and - in the case of de...

Full description

Published in: Electronic Communications of the European Association for the Study of Science and Technology
Published: 2013
Online Access: http://www.cs.swan.ac.uk/~csfm/avocs12.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa13712
first_indexed 2013-07-23T12:10:45Z
last_indexed 2018-02-09T04:44:35Z
id cronfa13712
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2015-07-01T09:18:58.5292147</datestamp><bib-version>v2</bib-version><id>13712</id><entry>2012-12-16</entry><title>Railway modelling in CSP||B: the double junction case study</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>This paper reports on recent work in verifying railway systems through CSP||B modelling and analysis. Our motivation is to develop a modelling and verification approach accessible to railway engineers: it is vital that they can validate the models and verification conditions, and - in the case of design errors - obtain comprehendable feedback. In this paper we run through a full production cycle on a real double junction case study, supplied by our industrial partner, who contributed at every stage. As our formalization is, by design, near to their way of thinking, they are comfortable with it and trust it. Without putting much effort on optimization for verification, the scale of the models analyzed is comparable with the work of other groups.</abstract><type>Journal Article</type><journal>Electronic Communications of the European Association for the Study of Science and Technology</journal><volume>n/a</volume><publisher/><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/avocs12.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:18:58.5292147</lastEdited><Created>2012-12-16T19:39:52.1576597</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:18:58.5292147 v2 13712 2012-12-16 Railway modelling in CSP||B: the double junction case study bf25e0b52fe7c11c473cc48d306073f7 0000-0001-9535-8053 Faron Moller Faron Moller true false 2012-12-16 MACS This paper reports on recent work in verifying railway systems through CSP||B modelling and analysis. Our motivation is to develop a modelling and verification approach accessible to railway engineers: it is vital that they can validate the models and verification conditions, and - in the case of design errors - obtain comprehendable feedback. In this paper we run through a full production cycle on a real double junction case study, supplied by our industrial partner, who contributed at every stage. As our formalization is, by design, near to their way of thinking, they are comfortable with it and trust it. Without putting much effort on optimization for verification, the scale of the models analyzed is comparable with the work of other groups. Journal Article Electronic Communications of the European Association for the Study of Science and Technology n/a formal methods, model checking, railway verification 31 12 2013 2013-12-31 http://www.cs.swan.ac.uk/~csfm/avocs12.pdf COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2015-07-01T09:18:58.5292147 2012-12-16T19:39:52.1576597 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 Railway modelling in CSP||B: the double junction case study
spellingShingle Railway modelling in CSP||B: the double junction case study
Faron Moller
title_short Railway modelling in CSP||B: the double junction case study
title_full Railway modelling in CSP||B: the double junction case study
title_fullStr Railway modelling in CSP||B: the double junction case study
title_full_unstemmed Railway modelling in CSP||B: the double junction case study
title_sort Railway modelling in CSP||B: the double junction case study
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 Journal article
container_title Electronic Communications of the European Association for the Study of Science and Technology
container_volume n/a
publishDate 2013
institution Swansea University
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/avocs12.pdf
document_store_str 0
active_str 0
description This paper reports on recent work in verifying railway systems through CSP||B modelling and analysis. Our motivation is to develop a modelling and verification approach accessible to railway engineers: it is vital that they can validate the models and verification conditions, and - in the case of design errors - obtain comprehendable feedback. In this paper we run through a full production cycle on a real double junction case study, supplied by our industrial partner, who contributed at every stage. As our formalization is, by design, near to their way of thinking, they are comfortable with it and trust it. Without putting much effort on optimization for verification, the scale of the models analyzed is comparable with the work of other groups.
published_date 2013-12-31T06:25:30Z
_version_ 1821385666648342528
score 10.969525

Similar Items