@inbook{16cbeed7999943ff9f7480b10cab7e27,
title = "Formal Verification of Railway Timetables - Using the UPPAAL Model Checker",
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{\ae}rumbanen in Denmark.",
keywords = "Formal methods, Model checking, Railways, Timetables, UPPAAL",
author = "Haxthausen, {Anne E.} and Kristian Hede",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-30985-5_25",
language = "English",
isbn = "978-3-030-30984-8",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "433--448",
booktitle = "From Software Engineering to Formal Methods and Tools, and Back",
}