Formal Verification of Railway Timetables - Using the UPPAAL Model Checker

Anne E. Haxthausen*, Kristian Hede

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

174 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationFrom Software Engineering to Formal Methods and Tools, and Back
Publication date1 Jan 2019
ISBN (Print)978-3-030-30984-8
Publication statusPublished - 1 Jan 2019
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11865 LNCS


  • Formal methods
  • Model checking
  • Railways
  • Timetables


Dive into the research topics of 'Formal Verification of Railway Timetables - Using the UPPAAL Model Checker'. Together they form a unique fingerprint.

Cite this