Formal Modelling and Veri fication of Railway Time Tables | Kristian Hede
| | 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] | | Year | 2012 | | Publisher | Technical University of Denmark, DTU Informatics, E-mail: reception@imm.dtu.dk | | Address | Asmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark | | Series | IMM-M.Sc.-2012-71 | | Note | Supervised by Associate Professor Anne Haxthausen, ah@imm.dtu.dk, DTU Informatics | | Electronic version(s) | [pdf] | | Publication link | http://www.imm.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|