Skip to main content

2016 | OriginalPaper | Buchkapitel

Static Verification of Railway Schema and Interlocking Design Data

verfasst von : Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah

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

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

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!

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!

Literatur
1.
Zurück zum Zitat 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) 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.
Zurück zum Zitat 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) 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.
Zurück zum Zitat 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 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.
Zurück zum Zitat 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 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.
Zurück zum Zitat Winter, K.: Model checking railway interlocking systems. In: Proceeding of the 25th Australian Computer Science Conference (ACSC 2002) (2002) Winter, K.: Model checking railway interlocking systems. In: Proceeding of the 25th Australian Computer Science Conference (ACSC 2002) (2002)
6.
Zurück zum Zitat Winter, K., Robinson, N.: Modelling large railway interlockings and model checking small ones. In: Proceeding of the Australian Cumputer Science Conference (ACSC 2003) (2003) 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.
Zurück zum Zitat Burdy, L.: Automatic refinement. In: Proceedings of BUGM at FM 1999 (1999) Burdy, L.: Automatic refinement. In: Proceedings of BUGM at FM 1999 (1999)
8.
Zurück zum Zitat Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. CoRR, abs/1210.6815 (2012) Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. CoRR, abs/1210.6815 (2012)
9.
Zurück zum Zitat 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 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
11.
Zurück zum Zitat 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 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
Metadaten
Titel
Static Verification of Railway Schema and Interlocking Design Data
verfasst von
Alexei Iliasov
Paulius Stankaitis
David Adjepon-Yamoah
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-33951-1_9

Premium Partner