View in EDS

Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods.

Saved in:
Bibliographic Details
Title: Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods.
Authors: Basile, Davide1 (AUTHOR) davide.basile@isti.cnr.it, ter Beek, Maurice H.1 (AUTHOR), Ferrari, Alessio1 (AUTHOR), Legay, Axel2 (AUTHOR)
Source: International Journal on Software Tools for Technology Transfer. Jun2022, Vol. 24 Issue 3, p351-370. 20p.
Subjects: Railroads, Joint ventures, Railroad trains, Statistical models
Abstract: Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/ETCS railway signalling systems that promise to move European railway forward by guaranteeing high capacity, low cost and improved reliability. We explore the ERTMS/ETCS level 3 full moving block specifications stemming from different Shift2Rail projects using Uppaal and statistical model checking. The results range from novel rigorously formalised requirements to an operational model formally verified against scenarios with multiple trains on a single railway line. From the gained experience, we have distilled future research goals to improve the formal specification and verification of real-time systems, and we discuss some barriers concerning a possible uptake of formal methods and tools in the railway industry. [ABSTRACT FROM AUTHOR]
Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 156802951
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Basile%2C+Davide%22">Basile, Davide</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> davide.basile@isti.cnr.it</i><br /><searchLink fieldCode="AR" term="%22ter+Beek%2C+Maurice+H%2E%22">ter Beek, Maurice H.</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Ferrari%2C+Alessio%22">Ferrari, Alessio</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Legay%2C+Axel%22">Legay, Axel</searchLink><relatesTo>2</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22International+Journal+on+Software+Tools+for+Technology+Transfer%22">International Journal on Software Tools for Technology Transfer</searchLink>. Jun2022, Vol. 24 Issue 3, p351-370. 20p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Railroads%22">Railroads</searchLink><br /><searchLink fieldCode="DE" term="%22Joint+ventures%22">Joint ventures</searchLink><br /><searchLink fieldCode="DE" term="%22Railroad+trains%22">Railroad trains</searchLink><br /><searchLink fieldCode="DE" term="%22Statistical+models%22">Statistical models</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/ETCS railway signalling systems that promise to move European railway forward by guaranteeing high capacity, low cost and improved reliability. We explore the ERTMS/ETCS level 3 full moving block specifications stemming from different Shift2Rail projects using Uppaal and statistical model checking. The results range from novel rigorously formalised requirements to an operational model formally verified against scenarios with multiple trains on a single railway line. From the gained experience, we have distilled future research goals to improve the formal specification and verification of real-time systems, and we discuss some barriers concerning a possible uptake of formal methods and tools in the railway industry. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=156802951
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10009-022-00653-3
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 20
        StartPage: 351
    Subjects:
      – SubjectFull: Railroads
        Type: general
      – SubjectFull: Joint ventures
        Type: general
      – SubjectFull: Railroad trains
        Type: general
      – SubjectFull: Statistical models
        Type: general
    Titles:
      – TitleFull: Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Basile, Davide
      – PersonEntity:
          Name:
            NameFull: ter Beek, Maurice H.
      – PersonEntity:
          Name:
            NameFull: Ferrari, Alessio
      – PersonEntity:
          Name:
            NameFull: Legay, Axel
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 06
              Text: Jun2022
              Type: published
              Y: 2022
          Identifiers:
            – Type: issn-print
              Value: 14332779
          Numbering:
            – Type: volume
              Value: 24
            – Type: issue
              Value: 3
          Titles:
            – TitleFull: International Journal on Software Tools for Technology Transfer
              Type: main
ResultId 1