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

Techniques for modelling and verifying railway interlockings

verfasst von: Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, Helen Treharne

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

We describe a novel framework for modelling railway interlockings which has been developed in conjunction with railway engineers. The modelling language used is CSP\(||\)B. Beyond the modelling we present a variety of abstraction techniques which make the analysis of medium- to large-scale networks feasible. The paper notably introduces a covering technique that allows railway scheme plans to be decomposed into a set of smaller scheme plans. The finitisation and topological abstraction techniques are extended from previous work and are given formal foundations. All three techniques are applicable to other modelling frameworks besides CSP\(||\)B. Being able to apply abstractions and simplifications on the domain model before performing model checking is the key strength of our approach. We demonstrate the use of the framework on a real-life, medium-size scheme plan.
Vorheriger Artikel Towards Model-Driven V&V assessment of railway control systems
Nächster Artikel Automated generation of formal safety conditions from railway interlocking tables

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
Anhänge
Nur mit Berechtigung zugänglich
Literatur
1.
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. CUP, Cambridge (1996)
2.
Abrial, J.-R.: Modeling in Event-B, chapter 17-Train System. CUP, Cambridge (2010)
3.
Antoni, M.: Practical formal validation method for interlocking or automated systems. In: 3rd International Workshop on Dependable Control of Discrete Systems (DCDS), 2011, pp. ix–x (2011)
4.
Bjørner, D.: Dynamics of railway nets: on an interface between automatic control and software engineering. Elsevier. In: CTS (2003)
5.
Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A., Tchaltsev, A.: Formal verification and validation of ERTMS industrial railway train spacing system. In: CAV, volume 7358 of LNCS, pp. 378–393. Springer (2012)
6.
Fantechi, A., Gnesi, S.: On the adoption of model checking in safety-related software industry. In: Computer Safety, Reliability, and Security, pp. 383–396 (2011)
7.
Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. FORMS/FORMAT 2010, 107–115 (2011)
8.
Fowler, M.: Domain Specific Languages. Addison-Wesley, Reading (2010)
9.
Haxthausen, A.E.: Automated generation of safety requirements from railway interlocking tables. In: ISoLA (2), volume 7610 of LNCS, pp. 261–275. Springer (2012)
10.
Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687–701 (2000)CrossRef
11.
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
12.
Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways-an approach in Timed CSP. In: IFM, pp. 54–68 (2012)
13.
Jacquart, R. (ed.): IFIP 18th World Computer Congress, Topical Sessions, chapter TRain: The Railway Domain-A Grand Challenge. Kluwer, Dordrecht (2004)
14.
James, P., Beckmann, A., Roggenbach, M.: Using domain specific languages to support verification in the railway domain. In: Proceedings of HVC’12: Eighth Haifa Verification Conference, LNCS. Springer (to appear)
15.
James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H. : On Modelling and Verifying Railway Interlockings: Tracking Train Lengths. Technical Report CS-13-03, University of Surrey, Department of Computing (2013)
16.
James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based modelchecking. ECEASST, 35 (2010)
17.
James, P., Trumble, M., Treharne, H., Roggenbach, M., Schneider, S.: OnTrack: an open tooling environment for railway verification. In: Proceedings of NFM’13: Fifth NASA Formal Methods Symposium (2013)
18.
Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlockings. Electron. Notes Theor. Comput. Sci. 250, 19–31 (2009)
19.
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRef
20.
Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Formal Asp. Comput. 23(6), 683–709 (2011)MathSciNetCrossRef
21.
Mernik, M., Heering, J., Sloane, A.M.: When and how to develop domain-specific languages. ACM Comput. Surv., 37(4) (2005)
22.
Moller, F., Nguyen, H.N., Roggenbach, M.: Covering for CSP. Swansea University, Technical report (2013)
23.
Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Combining Event-Based and State-Based Modelling for Railway Verification. Technical Report CS-12-02, University of Surrey (2012)
24.
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: Proceedings of HVC’12: Eighth Haifa Verification Conference, p. 16 (2012) (to appear in Springer Lecture Notes in Computer Science)
25.
Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Railway modelling in CSP\(\parallel \)B: The double junction case study. Electron. Commun. EASST, 53, 15 (2012)
26.
Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Using ProB and CSP\(\parallel \)B for railway modelling. In: Proceedings of IFM’12 and ABZ 2012 Posters and Tool demos session, pp. 31–35 (2012)
27.
Morgan. C.C.: Of wp and CSP. In: Beauty is Our Business: A Birthday Salute to Edsger J. Dijkstra, pp. 319–326. Springer (1990)
28.
Morley, M.J.: Safety in railway signalling data: a behavioural analysis. In: HOLTPA, pp. 464–474. Springer (1993)
29.
30.
Nock, O.-S.: Railway Signalling. IRSE (1980)
31.
32.
33.
Sabatier, D., Burdy, L., Requet, A., Guéry, J.: Formal proofs for the NYCT line 7 (flushing) modernization project. In: ABZ, pp. 369–372 (2012)
34.
Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Asp. Comput. 17(4), 390–422 (2005)CrossRefMATH
35.
Simpson, A., Woodcock, J., Davies, J.: The mechanical verification of solid-state interlocking geographic data. In: Formal Methods Pacific 97. Springer (1997)
36.
37.
Winter, K.: Model checking railway interlocking systems. Aust. Comput. Sci. Commun. 24(1) (2002)
38.
Winter, K., Robinson, N.: Modelling large railway interlockings and model checking small ones. In: Proceedings of the 26th Australasian Computer Science Conference-Volume 16, pp. 309–316. Australian Computer Society Inc, (2003)
Metadaten
Titel
Techniques for modelling and verifying railway interlockings
verfasst von
Phillip James
Faron Moller
Hoang Nga Nguyen
Markus Roggenbach
Steve Schneider
Helen Treharne
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-014-0304-7

Weitere Artikel der Ausgabe 6/2014

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

Regular Paper

Model checking evaluation of airplane landing trajectories

FMRCS

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

Regular Paper

Survey on test data generation tools

FMRCS

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

FMRCS

Automated generation of formal safety conditions from railway interlocking tables

Introduction

Formal methods for railway control systems

Premium Partner

    Bildnachweise