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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Research in optimisation models and techniques for generating optimal timetables have been done [6], but these are very rarely used by the railway operators.
- 2.
An interlocking system is a signalling system component responsible for the safe routing of trains through a railway network.
- 3.
In Denmark this is the case for most railway networks, with only very few exceptions.
- 4.
Note that the interlocking system has the responsibility to ensure that collisions would not happen in such cases.
- 5.
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.
- 6.
There is no space to show and explain the many auxiliary functions used in the edge labels to implement that.
- 7.
d can be found from s as explained in Sect. 4.4.
- 8.
The experiments were done with an Intel(R) Core(TM) i5-5200U processor at 2.2 GHz with 12 GB RAM.
References
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_2
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_7
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_15
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_13
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)
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)
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
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/S0167642316300570
Winter, K.: Symbolic model checking for interlocking systems. In: Flammini, F. (ed.) Railway Safety, Reliability, and Security: Technologies and Systems Engineering. IGI Global (2012)
Acknowledgements
This paper is dedicated to Professor Stefania Gnesi on the occasion of her 65th birthday. The first author has had the great pleasure of meeting Stefania Gnesi at many occasions and would like to thank her for inspiration, discussions, and collaboration, especially in European Technical Working Group on Formal Methods in Railway Control.
The research was partially funded by the RobustRailS project (2012-17) granted by Innovation Fund Denmark under grant agreement 0603-00483B. The authors are grateful to the organisers of the Festschrift Symposium for giving the opportunity to prepare this paper. We would like to thank the anonymous reviewers for their comments, and we would like to thank Alex Landex for discussions and sharing of his deep knowledge about railway timetabling while he was employed as a researcher in railway operations at DTU Transport.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Haxthausen, A.E., Hede, K. (2019). Formal Verification of Railway Timetables - Using the UPPAAL Model Checker. In: ter Beek, M., Fantechi, A., Semini, L. (eds) From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science(), vol 11865. Springer, Cham. https://doi.org/10.1007/978-3-030-30985-5_25
Download citation
DOI: https://doi.org/10.1007/978-3-030-30985-5_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30984-8
Online ISBN: 978-3-030-30985-5
eBook Packages: Computer ScienceComputer Science (R0)