Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 6/2014

01.11.2014 | FMRCS

Automated generation of formal safety conditions from railway interlocking tables

verfasst von: Anne E. Haxthausen

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2014

Einloggen

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

search-config
loading …

Abstract

This paper describes a tool for extracting formal safety conditions from interlocking tables for railway interlocking systems. The tool has been applied to generate safety conditions for the interlocking system at Stenstrup station in Denmark, and the SAL model checker tool has been used to check that these conditions were satisfied by a model of the relay circuits implementing the interlocking system at Stenstrup station.
Vorheriger Artikel Techniques for modelling and verifying railway interlockings
Nächster Artikel Survey on test data generation 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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Fußnoten
1
They are also used for some computer based interlocking systems.
 
2
More general Kripke models allow non-propositional variables provided these have finite domains. However, for the models presented in this article, propositional variables are sufficient.
 
3
In the models we are considering, there is only one possible initial state. More general Kripke structures allow for a set of initial states.
 
4
\(R\) is total means that for all \(s\in S\) there is a state \(s'\in S\) such that \((s,s')\in R\)
 
5
Note that we only consider SAL specifications for which the relation defined in this way is total (as required for Kripke structures). We use the SAL deadlock checker to check that.
 
6
Note: two routes can only share a locking relay when at least one point is required to be set in different positions for the two routes.
 
Literatur
1.
Aanæs, M., Thai, H.P.: Modelling and verification of relay interlocking systems. Technical Report IMM-MSC-2012-14, DTU Informatics. Master thesis supervised by Anne Haxthausen, ah@imm.dtu.dk, Technical University of Denmark (2012)
2.
Banci, M., Fantechi, A., Gnesi, S.: Some experiences on formal specification of railway interlocking systems using Statecharts (2005)
3.
Bjørner, D.: New results and current trends in formal techniques for the development of software for transportation systems. In: Tanai, G., Schnieder, E. (eds.) Proceedings of the Symposium on Formal Methods for Railway Operation and Control Systems (FORMS’2003), Budapest/Hungary. L’Harmattan Hongrie, 15–16 May 2003, pp. 3–22
4.
Bliguet, M.L., Kjær, A.A.: Modelling interlocking systems for railway stations. Technical Report IMM-M.Sc.-2008-68, DTU Informatics. Master thesis supervised by Anne Haxthausen, ah@imm.dtu.dk, Technical University of Denmark (2008)
5.
Cao, Y., Xu, T., Tang, T., Wang, H., Zhao, L.: Automatic generation and verification of interlocking tables based on domain specific language for computer based interlocking systems (DSL-CBI). In: Proceedings of the IEEE International Conference on Computer Science and Automation Engineering (CSAE 2011), pp. 511–515. IEEE (2011)
6.
Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press, Cambridge (1999)
7.
8.
Eriksson, L.-H.: Using formal methods in a retrospective safety case. In: Computer safety, reliability, and security—23rd International Conference, SAFECOMP 2004, volume 3219 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2004)
9.
European Committee for Electrotechnical Standardization: EN 50128:2011—Railway applications—communications, signalling and processing systems—software for railway control and protection systems. CENELEC, Brussels (2011)
10.
Fantechi, A.: The role of formal methods in software development for railway applications. In: Railway safety, reliability and security: technologies and system engineering, pp. 282–297. IGI Global, USA (2012)
11.
Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai G. (eds.) Proceedings of formal methods for automation and safety in railway and automotive systems (FORMS/FORMAT 2010). Springer, Berlin, Heidelberg (2011)
12.
Haxthausen, A.E.: Towards a framework for modelling and verification of relay interlocking systems. In: 16th Monterey Workshop: modelling, development and verification of adaptive systems: the grand challenge for robust software, number 6662 in Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2011) (Invited paper)
13.
Haxthausen, A.E., Bliguet, M.L., Kjær, A.A.: Modelling and verification of relay interlocking systems. In: Choppy, C., Sokolsky, O. (eds.) 15th Monterey Workshop: foundations of computer software, pp. 141–153. Future trends and techniques for development, number 6028 in Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2010) (Invited paper)
14.
Haxthausen, A.E., Kjær, A.A., Bliguet, M.L.: Formal development of a tool for automated modelling and verification of relay interlocking systems. In: 17th International Symposium on Formal Methods (FM 2011), number 6664 in Lecture Notes in Computer Science, pp. 118–132. Springer, Berlin, Heidelberg (2011)
15.
16.
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)CrossRef
17.
Mirabadi, A., Yazdi, M.B.: Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Transp. Probl. 4, 103–110 (2009)
18.
Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP\(\parallel \)B. In: Hardware and Software: Verification and Testing, 8th International Haifa Verification Conference, number 7857 in Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2013)
19.
Schnieder, E., Tarnai, G. (eds.): Proceedings of formal methods for automation and safety in railway and automotive systems (FORMS/FORMAT 2010). Springer, Berlin, Heidelberg (2011)
20.
21.
The RAISE Language Group: The RAISE specification language. The BCS Practitioners Series. Prentice Hall Int., UK (1992)
22.
The RAISE Method Group: The RAISE development method. The BCS Practitioners Series. Prentice Hall Int., UK (1995)
23.
Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA’2012), Part II, number 7610 in Lecture Notes in Computer Science, pp. 246–260. Springer, Berlin, Heidelberg (2012)
24.
Winter, K.: Symbolic model checking for interlocking systems. In: Railway safety, reliability and security: technologies and system engineering, pp. 298–315. IGI Global, USA (2012)
25.
Winter, K., Johnston, W., Robinson, P., Strooper, P., van den Berg, L.: Tool support for checking railway interlocking designs. In: Proceedings of the 10th Australian workshop on Safety Critical Systems and Software, vol. 55, SCS ’05, pp. 101–107. Australian Computer Society Inc., Darlinghurst (2006)
Metadaten
Titel
Automated generation of formal safety conditions from railway interlocking tables
verfasst von
Anne E. Haxthausen
Publikationsdatum
01.11.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 6/2014
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-013-0295-9

Weitere Artikel der Ausgabe 6/2014

International Journal on Software Tools for Technology Transfer 6/2014 Zur Ausgabe

FMRCS

From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions

Regular Paper

Survey on test data generation tools

Regular Paper

Model checking evaluation of airplane landing trajectories

FMRCS

Techniques for modelling and verifying railway interlockings

FMRCS

Towards Model-Driven V&V assessment of railway control systems

Introduction

Formal methods for railway control systems

Premium Partner

    Bildnachweise