nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Formal Verification of Railway Timetables - Using the UPPAAL Model Checker

verfasst von : Anne E. Haxthausen, Kristian Hede

Erschienen in: From Software Engineering to Formal Methods and Tools, and Back

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

This paper considers the challenge of validating railway timetables and investigates how formal methods can be used for that. The paper presents a re-configurable, formal model which can be configured with a timetable for a railway network, properties of that network, and various timetabling parameters (such as station and line capacities, headways, and minimum running times) constraining the allowed train behaviour. The formal model describes the system behaviour of trains driving according to the given railway timetable. Model checking can then be used to check that driving according to the timetable does not lead to illegal system states. The method has successfully been applied to a real world case study: a time table for 12 trains at Nærumbanen in Denmark.

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

Vorheriges Kapitel Hunting Superfluous Locks with Model Checking

Nächstes Kapitel An Axiomatization of Strong Distribution Bisimulation for a Language with a Parallel Operator and Probabilistic Choice

Research in optimisation models and techniques for generating optimal timetables have been done [6], but these are very rarely used by the railway operators.

An interlocking system is a signalling system component responsible for the safe routing of trains through a railway network.

In Denmark this is the case for most railway networks, with only very few exceptions.

Note that the interlocking system has the responsibility to ensure that collisions would not happen in such cases.

To allow for different minimum dwell times at the same station for different trains, this scheduling parameter has been placed here and not in stationTable.

There is no space to show and explain the many auxiliary functions used in the edge labels to implement that.

d can be found from s as explained in Sect. 4.4.

The experiments were done with an Intel(R) Core(TM) i5-5200U processor at 2.2 GHz with 12 GB RAM.

Banci, M., Fantechi, A., Gnesi, S.: Some experiences on formal specification of railway interlocking systems using statecharts. In: TRain Workshop at SEFM (2005)

Basile, D., et al.: On the industrial uptake of formal methods in the railway domain - a survey with stakeholders. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 20–29. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_2CrossRef

Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7CrossRef

Di Giandomenico, F., Fantechi, A., Gnesi, S., Itria, M.L.: Stochastic model-based analysis of railway operation to support traffic planning. In: Gorbenko, A., Romanovsky, A., Kharchenko, V. (eds.) SERENE 2013. LNCS, vol. 8166, pp. 184–198. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40894-6_15CrossRef

Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167–183. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05032-4_13CrossRef

Hansen, I.A., Pachl, J.: Railway timetable & traffic: analysis, modelling, simulation. Eurailpress (2008)

James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Techniques for modelling and verifying railway interlockings. Int. J. Softw. Tools Technol. Transf. 16(6), 685–711 (2014)CrossRef

Khan, U., Ahmad, J., Saeed, T., Hayat, S.: Real time modeling of interlocking control system of Rawalpindi Cantt train yard. In: 2015 13th International Conference on Frontiers of Information Technology (FIT), pp. 347–352 (2015). https://doi.org/10.1109/FIT.2015.28

Landex, A., Kaas, A., Hansen, S.: Railway Operation. Technical report, Technical University of Denmark, Centre for Traffic and Transport (2006)

10.

Schittenhelm, B., Landex, A.: Jernbanesimuleringsværktøjer i Danmark (Eng.: Railway Simulation Tools in Denmark). Aalborg Trafikdage (2008) (in Danish). www.trafikdage.dk/papers_2008/praesentationer/bernd_schittenhelm_158.pdf

11.

Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, Part 2, 91–115 (2017). https://doi.org/10.1016/j.scico.2016.05.010. http://www.sciencedirect.com/science/article/pii/S0167642316300570CrossRef

12.

Winter, K.: Symbolic model checking for interlocking systems. In: Flammini, F. (ed.) Railway Safety, Reliability, and Security: Technologies and Systems Engineering. IGI Global (2012)

Titel: Formal Verification of Railway Timetables - Using the UPPAAL Model Checker
verfasst von: Anne E. Haxthausen
Kristian Hede
Verlag: Springer International Publishing
Buch: From Software Engineering to Formal Methods and Tools, and Back
Print ISBN: 978-3-030-30984-8

Electronic ISBN: 978-3-030-30985-5

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30985-5_25

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner