Hide metadata

dc.date.accessioned2018-03-13T14:27:40Z
dc.date.available2018-03-13T14:27:40Z
dc.date.created2017-10-18T09:37:56Z
dc.date.issued2017
dc.identifier.citationLuteberget, Bjørnar Steinnes Johansen, Christian . Efficient verification of railway infrastructure designs against standard regulations. Formal methods in system design. 2017, 1-32
dc.identifier.urihttp://hdl.handle.net/10852/60945
dc.description.abstractIn designing safety-critical infrastructures s.a. railway systems, engineers often have to deal with complex and large-scale designs. Formal methods can play an important role in helping automate various tasks. For railway designs formal methods have mainly been used to verify the safety of so-called interlockings through model checking, which deals with state change and rather complex properties, usually incurring considerable computational burden (e.g., the state-space explosion problem). In contrast, we focus on static infrastructure models, and are interested in checking requirements coming from design guidelines and regulations, as usually given by railway authorities or safety certification bodies. Our goal is to automate the tedious manual work that railway engineers do when ensuring compliance with regulations, through using software that is fast enough to do verification on-the-fly, thus being able to be included in the railway design tools, much like a compiler in an IDE. In consequence, this paper describes the integration into the railway design process of formal methods for automatically extracting railway models from the CAD railway designs and for describing relevant technical regulations and expert knowledge as properties to be checked on the models. We employ a variant of Datalog and use the standardized “railway markup language” railML as basis and exchange format for the formalization. We developed a prototype tool and integrated it in industrial railway CAD software, developed under the name RailCOMPLETE®. This on-the-fly verification tool is a help for the engineer while doing the designs, and is not a replacement to other more heavy-weight software like for doing interlocking verification or capacity analysis. Our tool, through the export into railML, can be easily integrated with these other tools. We apply our tool chain in a Norwegian railway project, the upgrade of the Arna railway station.en_US
dc.languageEN
dc.rightsAttribution 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.titleEfficient verification of railway infrastructure designs against standard regulationsen_US
dc.typeJournal articleen_US
dc.creator.authorLuteberget, Bjørnar Steinnes
dc.creator.authorJohansen, Christian
cristin.unitcode185,15,5,32
cristin.unitnameForskningsgruppen for presis modellering og analyse
cristin.ispublishedtrue
cristin.fulltextoriginal
cristin.qualitycode2
dc.identifier.cristin1505423
dc.identifier.bibliographiccitationinfo:ofi/fmt:kev:mtx:ctx&ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.jtitle=Formal methods in system design&rft.volume=&rft.spage=1&rft.date=2017
dc.identifier.jtitleFormal methods in system design
dc.identifier.startpage1
dc.identifier.endpage32
dc.identifier.doihttp://dx.doi.org/10.1007/s10703-017-0281-z
dc.identifier.urnURN:NBN:no-63575
dc.type.documentTidsskriftartikkelen_US
dc.type.peerreviewedPeer reviewed
dc.source.issn0925-9856
dc.identifier.fulltextFulltext https://www.duo.uio.no/bitstream/handle/10852/60945/1/FMSD_journal_version.pdf
dc.type.versionPublishedVersion
dc.relation.projectNFR/248714


Files in this item

Appears in the following Collection

Hide metadata

Attribution 4.0 International
This item's license is: Attribution 4.0 International