Formal Modelling and Verification of Railway Time Tables
|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.
|Type||Master's thesis [Academic thesis]|
|Publisher||Technical University of Denmark, DTU Informatics, E-mail: email@example.com|
|Address||Asmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark|
|Note||Supervised by Associate Professor Anne Haxthausen, firstname.lastname@example.org, DTU Informatics|
|BibTeX data|| [bibtex]|
|IMM Group(s)||Computer Science & Engineering|
Back :: IMM Publications