@MASTERSTHESIS\{IMM2012-06349,
    author       = "K. Hede",
    title        = "Formal Modelling and Verification of Railway Time Tables",
    year         = "2012",
    school       = "Technical University of Denmark, {DTU} Informatics, {E-}mail: reception@imm.dtu.dk",
    address      = "Asmussens Alle, Building 305, {DK-}2800 Kgs. Lyngby, Denmark",
    type         = "",
    note         = "Supervised by Associate Professor Anne Haxthausen, ah@imm.dtu.dk, {DTU} Informatics",
    url          = "http://www.imm.dtu.dk/English.aspx",
    abstract     = "The 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."
}