Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
The Risk Assessment of ERTMS-Based Railway Systems from a Cyber Security Perspective: Methodology and Lessons Learned Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Static Verification of Railway Schema and Interlocking Design Data

Authors : Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah

Published in: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The paper presents an experience of verifying a large scale, real-life dataset describing various aspects of railway station design. We discuss how a number of assorted digital artefacts were pooled together and converted into a set-theoretic model over which a type inference procedure is run. The typed model is then used to confirm or contradict logical conjectures over data elements. We employ a number of state-of-the-art SMT solvers as a verification back-end. The project is ongoing but has already identified a number of issues in topology definition and signalling data that were missed by other automated tests and not revealed by simulation tools.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models
next chapter Verification of Railway Interlocking - Compositional Approach with OCRA
Literature
1.
Iliasov, A., Lopatkin, I., Romanovsky, A.: Practical formal methods in railways - the SafeCap approach. In: George, L., Vardanega, T. (eds.) Ada-Europe 2014. LNCS, vol. 8454, pp. 177–192. Springer, Heidelberg (2014)
2.
Janczura, C.W.: Modelling and Analysis of Railway Network Control Logic using Coloured Petri Nets. PhD thesis, School of Mathematics and Institute for Telecommunications Research, University of South Australia (1998)
3.
Hagalisletto, A.M., Bjørk, J., Chieh Yu, I., Enger, P.: Constructing and refining large-scale railway models represented by Petri Nets. IEEE Trans. Syst. Man Cybern. Part C 37, 444–460 (2007)CrossRef
4.
Iliasov, A., Romanovsky, A.: SafeCap domain language for reasoning about safety and capacity. In: Pacific-Rim Dependable Computing Conference (PRDC 2012), Niigata, Japan. IEEE CS, November 2012
5.
Winter, K.: Model checking railway interlocking systems. In: Proceeding of the 25th Australian Computer Science Conference (ACSC 2002) (2002)
6.
Winter, K., Robinson, N.: Modelling large railway interlockings and model checking small ones. In: Proceeding of the Australian Cumputer Science Conference (ACSC 2003) (2003)
7.
Burdy, L.: Automatic refinement. In: Proceedings of BUGM at FM 1999 (1999)
8.
Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. CoRR, abs/1210.6815 (2012)
9.
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)CrossRef
10.
11.
Abo, R., Voisin, L.: Formal implementation of data validation for railway safety-related systems with OVADO. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 221–236. Springer, Heidelberg (2014)CrossRef
12.
13.
Metadata
Title
Static Verification of Railway Schema and Interlocking Design Data
Authors
Alexei Iliasov
Paulius Stankaitis
David Adjepon-Yamoah
Copyright Year
2016
Book
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification

Print ISBN: 978-3-319-33950-4

Electronic ISBN: 978-3-319-33951-1

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-33951-1_9

Premium Partner

    Image Credits