No Cover Image

Conference Paper/Proceeding/Abstract 511 views

Decomposing scheme plans to manage verification complexity

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

FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems

Swansea University Authors: Phillip James Orcid Logo, Faron Moller Orcid Logo, Hoang Nguyen Orcid Logo, Markus Roggenbach Orcid Logo

Abstract

Several formal methods have been proposed for the specification and safety verification of railway applications. In order to be successful they need industrial strength tools to support the animation, proof, model checking and simulation of such systems. The complexity of railway systems means that...

Full description

Published in: FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems
Published: 2014
URI: https://cronfa.swan.ac.uk/Record/cronfa37077
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2017-11-27T16:02:15Z
last_indexed 2023-01-11T14:12:18Z
id cronfa37077
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2022-12-07T10:20:47.0125940</datestamp><bib-version>v2</bib-version><id>37077</id><entry>2017-11-27</entry><title>Decomposing scheme plans to manage verification complexity</title><swanseaauthors><author><sid>fd3b15ff96c5ea91a100131abac558b6</sid><ORCID>0000-0002-4307-649X</ORCID><firstname>Phillip</firstname><surname>James</surname><name>Phillip James</name><active>true</active><ethesisStudent>false</ethesisStudent></author><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><author><sid>cb24d5c5080534dc5b5e3390f24dd422</sid><ORCID>0000-0003-0260-1697</ORCID><firstname>Hoang</firstname><surname>Nguyen</surname><name>Hoang Nguyen</name><active>true</active><ethesisStudent>false</ethesisStudent></author><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></swanseaauthors><date>2017-11-27</date><deptcode>SCS</deptcode><abstract>Several formal methods have been proposed for the specification and safety verification of railway applications. In order to be successful they need industrial strength tools to support the animation, proof, model checking and simulation of such systems. The complexity of railway systems means that capabilities of the analysis tools have consistently been improving. In our approach we propose that the complexity of analysis of railway interlocking systems can also be managed through incremental addition of system detail and decomposition of system specifications themselves. We propose a domain specific language (DSL) which describes the core aspects of a railway interlocking system and demonstrate how one can identify suitable decompositions in terms of the DSL. The DSL informs our system engineering approach which uses a graphical editor to input railway scheme plans, supports the automatic generation of CSP jj B specifications of the plans and uses the ProB tool for their animation and model checking.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>1</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-01-01</publishedDate><doi/><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2022-12-07T10:20:47.0125940</lastEdited><Created>2017-11-27T11:02:49.3184898</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>Phillip</firstname><surname>James</surname><orcid>0000-0002-4307-649X</orcid><order>1</order></author><author><firstname>Faron</firstname><surname>Moller</surname><orcid>0000-0001-9535-8053</orcid><order>2</order></author><author><firstname>Hoang</firstname><surname>Nguyen</surname><orcid>0000-0003-0260-1697</orcid><order>3</order></author><author><firstname>Markus</firstname><surname>Roggenbach</surname><orcid>0000-0002-3819-2787</orcid><order>4</order></author><author><firstname>Steve</firstname><surname>Schneider</surname><order>5</order></author><author><firstname>Helen</firstname><surname>Treharne</surname><order>6</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2022-12-07T10:20:47.0125940 v2 37077 2017-11-27 Decomposing scheme plans to manage verification complexity fd3b15ff96c5ea91a100131abac558b6 0000-0002-4307-649X Phillip James Phillip James true false bf25e0b52fe7c11c473cc48d306073f7 0000-0001-9535-8053 Faron Moller Faron Moller true false cb24d5c5080534dc5b5e3390f24dd422 0000-0003-0260-1697 Hoang Nguyen Hoang Nguyen true false 7733869ae501442da6926fac77cd155b 0000-0002-3819-2787 Markus Roggenbach Markus Roggenbach true false 2017-11-27 SCS Several formal methods have been proposed for the specification and safety verification of railway applications. In order to be successful they need industrial strength tools to support the animation, proof, model checking and simulation of such systems. The complexity of railway systems means that capabilities of the analysis tools have consistently been improving. In our approach we propose that the complexity of analysis of railway interlocking systems can also be managed through incremental addition of system detail and decomposition of system specifications themselves. We propose a domain specific language (DSL) which describes the core aspects of a railway interlocking system and demonstrate how one can identify suitable decompositions in terms of the DSL. The DSL informs our system engineering approach which uses a graphical editor to input railway scheme plans, supports the automatic generation of CSP jj B specifications of the plans and uses the ProB tool for their animation and model checking. Conference Paper/Proceeding/Abstract FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems 1 1 2014 2014-01-01 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2022-12-07T10:20:47.0125940 2017-11-27T11:02:49.3184898 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Phillip James 0000-0002-4307-649X 1 Faron Moller 0000-0001-9535-8053 2 Hoang Nguyen 0000-0003-0260-1697 3 Markus Roggenbach 0000-0002-3819-2787 4 Steve Schneider 5 Helen Treharne 6
title Decomposing scheme plans to manage verification complexity
spellingShingle Decomposing scheme plans to manage verification complexity
Phillip James
Faron Moller
Hoang Nguyen
Markus Roggenbach
title_short Decomposing scheme plans to manage verification complexity
title_full Decomposing scheme plans to manage verification complexity
title_fullStr Decomposing scheme plans to manage verification complexity
title_full_unstemmed Decomposing scheme plans to manage verification complexity
title_sort Decomposing scheme plans to manage verification complexity
author_id_str_mv fd3b15ff96c5ea91a100131abac558b6
bf25e0b52fe7c11c473cc48d306073f7
cb24d5c5080534dc5b5e3390f24dd422
7733869ae501442da6926fac77cd155b
author_id_fullname_str_mv fd3b15ff96c5ea91a100131abac558b6_***_Phillip James
bf25e0b52fe7c11c473cc48d306073f7_***_Faron Moller
cb24d5c5080534dc5b5e3390f24dd422_***_Hoang Nguyen
7733869ae501442da6926fac77cd155b_***_Markus Roggenbach
author Phillip James
Faron Moller
Hoang Nguyen
Markus Roggenbach
author2 Phillip James
Faron Moller
Hoang Nguyen
Markus Roggenbach
Steve Schneider
Helen Treharne
format Conference Paper/Proceeding/Abstract
container_title FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems
publishDate 2014
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
document_store_str 0
active_str 0
description Several formal methods have been proposed for the specification and safety verification of railway applications. In order to be successful they need industrial strength tools to support the animation, proof, model checking and simulation of such systems. The complexity of railway systems means that capabilities of the analysis tools have consistently been improving. In our approach we propose that the complexity of analysis of railway interlocking systems can also be managed through incremental addition of system detail and decomposition of system specifications themselves. We propose a domain specific language (DSL) which describes the core aspects of a railway interlocking system and demonstrate how one can identify suitable decompositions in terms of the DSL. The DSL informs our system engineering approach which uses a graphical editor to input railway scheme plans, supports the automatic generation of CSP jj B specifications of the plans and uses the ProB tool for their animation and model checking.
published_date 2014-01-01T03:46:35Z
_version_ 1763752222768758784
score 11.013731

Similar Items