View in EDS PDF Full Text

Verification of Railway Control Systems Using Model Checking and CTL, Explained Through a Case Study.

Saved in:
Bibliographic Details
Title: Verification of Railway Control Systems Using Model Checking and CTL, Explained Through a Case Study.
Authors: Lukács, Gábor1 lukacs.gabor@edu.bme.hu, Bartha, Tamás1,2
Source: Periodica Polytechnica: Transportation Engineering. 2024, Vol. 52 Issue 4, p402-411. 10p.
Subjects: Railroad design & construction, Design failures, Systems engineering, Engineering design, Simulation methods & models
Abstract: Systematic faults can often occur during the development of a system. The later such faults are discovered, the more expensive it can be to correct them. In systems engineering practice, there are many methods and tools to reduce the likelihood of systematic faults. In this paper, we present the application of a formal model-based verification technique - called model checking - to assist railway engineers in designing and verifying the safety-related functionality of railway control systems. The proposed process is part of a specification-verification environment that facilitates the construction of correct, complete, consistent, and verifiable functional specifications during development. The results and experience in model checking are illustrated by a case study of a vehicle detection point, a common component in this domain. The model checking of the case study has been performed in the widely used UPPAAL modeling and simulation framework, which can also verify formal properties and generate a counterexample in case of a property violation. By analyzing the counterexample, the designer can gain insights into the system's behavior and identify potential design flaws or failures. Model checking can be used to achieve a higher quality functional specification that is typically more complete and/or contains fewer faults compared to the traditional development approach. [ABSTRACT FROM AUTHOR]
Copyright of Periodica Polytechnica: Transportation Engineering is the property of Periodica Polytechnica 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 Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 181587823
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Verification of Railway Control Systems Using Model Checking and CTL, Explained Through a Case Study.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Lukács%2C+Gábor%22">Lukács, Gábor</searchLink><relatesTo>1</relatesTo><i> lukacs.gabor@edu.bme.hu</i><br /><searchLink fieldCode="AR" term="%22Bartha%2C+Tamás%22">Bartha, Tamás</searchLink><relatesTo>1,2</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Periodica+Polytechnica%3A+Transportation+Engineering%22">Periodica Polytechnica: Transportation Engineering</searchLink>. 2024, Vol. 52 Issue 4, p402-411. 10p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Railroad+design+%26+construction%22">Railroad design & construction</searchLink><br /><searchLink fieldCode="DE" term="%22Design+failures%22">Design failures</searchLink><br /><searchLink fieldCode="DE" term="%22Systems+engineering%22">Systems engineering</searchLink><br /><searchLink fieldCode="DE" term="%22Engineering+design%22">Engineering design</searchLink><br /><searchLink fieldCode="DE" term="%22Simulation+methods+%26+models%22">Simulation methods & models</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Systematic faults can often occur during the development of a system. The later such faults are discovered, the more expensive it can be to correct them. In systems engineering practice, there are many methods and tools to reduce the likelihood of systematic faults. In this paper, we present the application of a formal model-based verification technique - called model checking - to assist railway engineers in designing and verifying the safety-related functionality of railway control systems. The proposed process is part of a specification-verification environment that facilitates the construction of correct, complete, consistent, and verifiable functional specifications during development. The results and experience in model checking are illustrated by a case study of a vehicle detection point, a common component in this domain. The model checking of the case study has been performed in the widely used UPPAAL modeling and simulation framework, which can also verify formal properties and generate a counterexample in case of a property violation. By analyzing the counterexample, the designer can gain insights into the system's behavior and identify potential design flaws or failures. Model checking can be used to achieve a higher quality functional specification that is typically more complete and/or contains fewer faults compared to the traditional development approach. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Periodica Polytechnica: Transportation Engineering is the property of Periodica Polytechnica 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=181587823
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.3311/PPtr.23344
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 10
        StartPage: 402
    Subjects:
      – SubjectFull: Railroad design & construction
        Type: general
      – SubjectFull: Design failures
        Type: general
      – SubjectFull: Systems engineering
        Type: general
      – SubjectFull: Engineering design
        Type: general
      – SubjectFull: Simulation methods & models
        Type: general
    Titles:
      – TitleFull: Verification of Railway Control Systems Using Model Checking and CTL, Explained Through a Case Study.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Lukács, Gábor
      – PersonEntity:
          Name:
            NameFull: Bartha, Tamás
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 10
              Text: 2024
              Type: published
              Y: 2024
          Identifiers:
            – Type: issn-print
              Value: 03037800
          Numbering:
            – Type: volume
              Value: 52
            – Type: issue
              Value: 4
          Titles:
            – TitleFull: Periodica Polytechnica: Transportation Engineering
              Type: main
ResultId 1