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)

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.

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

Keywords

  • Formal methods
  • Model checking
  • Railways
  • Timetables
  • UPPAAL

Fingerprint

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

Cite this