Formal Modelling and Verification of Railway Time Tables

Kristian Hede

AbstractThe goal of the thesis is to investigate how formal methods can be used to verify and create railway timetables.
First a formal model of railway networks and timetables in RSL is created. Based on the formal model of RSL, a model in UPPAAL is created, which is able to verify properties of existing timetables. A model in UPPAAL CORA is then created, which is able to generate timetables, which satisfy the same properties as those of the UPPAAL model.
Lastly a tool written in Java is created, which provides a graphical user interface for creating timetables. The tool uses UPPAAL CORA and the created model for creating timetables, and is able to visualize results. This tool is considered a prototype, and is an example of how for methods can be used to create timetables.
TypeMaster's thesis [Academic thesis]
PublisherTechnical University of Denmark, DTU Informatics, E-mail:
AddressAsmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark
NoteSupervised by Associate Professor Anne Haxthausen,, DTU Informatics
Electronic version(s)[pdf]
Publication link
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering

Back  ::  IMM Publications