No Cover Image

Journal article 446 views 69 downloads

OnTrack: Reflecting on domain specific formal methods for railway designs

Phillip James Orcid Logo, Faron Moller Orcid Logo, Filippos Pantekis Orcid Logo

Science of Computer Programming, Volume: 233, Start page: 103057

Swansea University Authors: Phillip James Orcid Logo, Faron Moller Orcid Logo, Filippos Pantekis Orcid Logo

  • 65127_FPantekis_VOR.pdf

    PDF | Version of Record

    This is an open access article distributed under the terms of the Creative Commons CC-BY license, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

    Download (1.14MB)

Check full text

DOI (Published version): 10.1016/j.scico.2023.103057

Abstract

OnTrack is a tool that supports workflows for railway verification that has been implemented using model driven engineering frameworks. Starting with graphical scheme plans and finishing with automatically generated formal models set-up for verification, OnTrack allows railway engineers to interact...

Full description

Published in: Science of Computer Programming
ISSN: 0167-6423 1872-7964
Published: Elsevier BV 2023
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa65127
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2023-11-27T14:48:37Z
last_indexed 2023-11-27T14:48:37Z
id cronfa65127
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>65127</id><entry>2023-11-27</entry><title>OnTrack: Reflecting on domain specific formal methods for railway designs</title><swanseaauthors><author><sid>3ded05e11923bacd96ee3ddea58b62bd</sid><ORCID>NULL</ORCID><firstname>Phillip</firstname><surname>James</surname><name>Phillip James</name><active>true</active><ethesisStudent>true</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>7e3976bc926b363ee1346c423ba74d11</sid><ORCID>0000-0001-7817-6450</ORCID><firstname>Filippos</firstname><surname>Pantekis</surname><name>Filippos Pantekis</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2023-11-27</date><abstract>OnTrack is a tool that supports workflows for railway verification that has been implemented using model driven engineering frameworks. Starting with graphical scheme plans and finishing with automatically generated formal models set-up for verification, OnTrack allows railway engineers to interact with verification procedures through encapsulating formal methods. OnTrack is grounded on a domain specification language (DSL) capturing scheme plans and supports generation of various formal models using model transformations. In this paper, we detail the role model driven engineering takes within OnTrack and reflect on the use of model driven engineering concepts for developing domain specific formal methods toolsets.</abstract><type>Journal Article</type><journal>Science of Computer Programming</journal><volume>233</volume><journalNumber/><paginationStart>103057</paginationStart><paginationEnd/><publisher>Elsevier BV</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>0167-6423</issnPrint><issnElectronic>1872-7964</issnElectronic><keywords>Model driven engineering, Formal methods, Railway verification</keywords><publishedDay>21</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-11-21</publishedDate><doi>10.1016/j.scico.2023.103057</doi><url>http://dx.doi.org/10.1016/j.scico.2023.103057</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><apcterm>SU Library paid the OA fee (TA Institutional Deal)</apcterm><funders>The authors would like to thank Siemens Rail Automation UK and the Rail Safety and Standards Board, RSSB, for supporting this work. We also wish to highlight the rich insights provided by Simon Chadwick, Mark Thomas, Thomas Werner and Andrew Lawrence from Siemens Rail Automation UK. We extend a special thanks to our academic collaborators, in particular, Prof. Markus Roggenbach, Dr. Hoang Nga Nguyen, Prof. Helen Treharne and Dr. Monika Seisenberger for their valued insights and contributions to the development of OnTrack.</funders><projectreference/><lastEdited>2024-01-03T12:41:08.3517195</lastEdited><Created>2023-11-27T14:41:16.4187962</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>NULL</orcid><order>1</order></author><author><firstname>Faron</firstname><surname>Moller</surname><orcid>0000-0001-9535-8053</orcid><order>2</order></author><author><firstname>Filippos</firstname><surname>Pantekis</surname><orcid>0000-0001-7817-6450</orcid><order>3</order></author></authors><documents><document><filename>65127__29118__4412c71d0ec544ecb6941f800a0ef2d6.pdf</filename><originalFilename>65127_FPantekis_VOR.pdf</originalFilename><uploaded>2023-11-27T14:45:44.1402984</uploaded><type>Output</type><contentLength>1196141</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>This is an open access article distributed under the terms of the Creative Commons CC-BY license, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling v2 65127 2023-11-27 OnTrack: Reflecting on domain specific formal methods for railway designs 3ded05e11923bacd96ee3ddea58b62bd NULL Phillip James Phillip James true true bf25e0b52fe7c11c473cc48d306073f7 0000-0001-9535-8053 Faron Moller Faron Moller true false 7e3976bc926b363ee1346c423ba74d11 0000-0001-7817-6450 Filippos Pantekis Filippos Pantekis true false 2023-11-27 OnTrack is a tool that supports workflows for railway verification that has been implemented using model driven engineering frameworks. Starting with graphical scheme plans and finishing with automatically generated formal models set-up for verification, OnTrack allows railway engineers to interact with verification procedures through encapsulating formal methods. OnTrack is grounded on a domain specification language (DSL) capturing scheme plans and supports generation of various formal models using model transformations. In this paper, we detail the role model driven engineering takes within OnTrack and reflect on the use of model driven engineering concepts for developing domain specific formal methods toolsets. Journal Article Science of Computer Programming 233 103057 Elsevier BV 0167-6423 1872-7964 Model driven engineering, Formal methods, Railway verification 21 11 2023 2023-11-21 10.1016/j.scico.2023.103057 http://dx.doi.org/10.1016/j.scico.2023.103057 COLLEGE NANME Computer Science COLLEGE CODE Swansea University SU Library paid the OA fee (TA Institutional Deal) The authors would like to thank Siemens Rail Automation UK and the Rail Safety and Standards Board, RSSB, for supporting this work. We also wish to highlight the rich insights provided by Simon Chadwick, Mark Thomas, Thomas Werner and Andrew Lawrence from Siemens Rail Automation UK. We extend a special thanks to our academic collaborators, in particular, Prof. Markus Roggenbach, Dr. Hoang Nga Nguyen, Prof. Helen Treharne and Dr. Monika Seisenberger for their valued insights and contributions to the development of OnTrack. 2024-01-03T12:41:08.3517195 2023-11-27T14:41:16.4187962 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Phillip James NULL 1 Faron Moller 0000-0001-9535-8053 2 Filippos Pantekis 0000-0001-7817-6450 3 65127__29118__4412c71d0ec544ecb6941f800a0ef2d6.pdf 65127_FPantekis_VOR.pdf 2023-11-27T14:45:44.1402984 Output 1196141 application/pdf Version of Record true This is an open access article distributed under the terms of the Creative Commons CC-BY license, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. true eng https://creativecommons.org/licenses/by/4.0/
title OnTrack: Reflecting on domain specific formal methods for railway designs
spellingShingle OnTrack: Reflecting on domain specific formal methods for railway designs
Phillip James
Faron Moller
Filippos Pantekis
title_short OnTrack: Reflecting on domain specific formal methods for railway designs
title_full OnTrack: Reflecting on domain specific formal methods for railway designs
title_fullStr OnTrack: Reflecting on domain specific formal methods for railway designs
title_full_unstemmed OnTrack: Reflecting on domain specific formal methods for railway designs
title_sort OnTrack: Reflecting on domain specific formal methods for railway designs
author_id_str_mv 3ded05e11923bacd96ee3ddea58b62bd
bf25e0b52fe7c11c473cc48d306073f7
7e3976bc926b363ee1346c423ba74d11
author_id_fullname_str_mv 3ded05e11923bacd96ee3ddea58b62bd_***_Phillip James
bf25e0b52fe7c11c473cc48d306073f7_***_Faron Moller
7e3976bc926b363ee1346c423ba74d11_***_Filippos Pantekis
author Phillip James
Faron Moller
Filippos Pantekis
author2 Phillip James
Faron Moller
Filippos Pantekis
format Journal article
container_title Science of Computer Programming
container_volume 233
container_start_page 103057
publishDate 2023
institution Swansea University
issn 0167-6423
1872-7964
doi_str_mv 10.1016/j.scico.2023.103057
publisher Elsevier BV
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.1016/j.scico.2023.103057
document_store_str 1
active_str 0
description OnTrack is a tool that supports workflows for railway verification that has been implemented using model driven engineering frameworks. Starting with graphical scheme plans and finishing with automatically generated formal models set-up for verification, OnTrack allows railway engineers to interact with verification procedures through encapsulating formal methods. OnTrack is grounded on a domain specification language (DSL) capturing scheme plans and supports generation of various formal models using model transformations. In this paper, we detail the role model driven engineering takes within OnTrack and reflect on the use of model driven engineering concepts for developing domain specific formal methods toolsets.
published_date 2023-11-21T12:41:10Z
_version_ 1787073051270053888
score 11.037581

Similar Items