@MASTERSTHESIS\{IMM2017-07009,
    author       = "C. Erdogan",
    title        = "Development of Tool Support for Compositional Verification of Railway Interlocking Systems",
    year         = "2017",
    school       = "Technical University of Denmark, Department of Applied Mathematics and Computer Science",
    address      = "Richard Petersens Plads, Building 324, {DK-}2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk",
    type         = "",
    note         = "{DTU} supervisor: Anne Haxthausen, aeha@dtu.dk, {DTU} Compute",
    url          = "http://www.compute.dtu.dk/English.aspx",
    abstract     = "This thesis describes the entire development of a decomposition tool, supporting the RobustRailS’ compositional verification of railway interlocking systems. 
Running a verification process with big railway networks can be a problem due to the state space explosion problem. A decomposition of railway systems can significantly reduce the verification time and increase the success rate of execution. With the tool developed in this project, the verification tool is supported for large scale industrial use by letting users easily decompose networks into smaller chunks.
A divide strategy called border cut is presented along with different approaches on how to apply this cut. The tool is designed to easily be extended with new types of cuts. Therefore, other divide strategies are also introduced as potential future extensions.
The {RAISE} Specification Language (RSL) is used to assist in the specification and design of the software. Starting from abstract specifications and developing them into concrete specifications, remarkably contributes to the overall quality of the product. Furthermore, development processes such as test-driven development (TDD) has been used to encourage simple design and confidence in the product.
The end product is a command line interface tool that accepts networks defined in {XML} and generates new {XML} files containing the sub-networks. Multiple experiments with self-created and real-world networks show that the tool can handle networks of different sizes, providing a very smooth user experience as well."
}