Improving formal analysis of computerised rail traffic control systems using domain models

Abstract: During the formal analysis of a computerized railway control system, it may be difficult to understand if a found counterexample to a requirement is a scenario which can happen in the real world or not. By putting sensible constraints on the inputs to the system, i.e. by defining a domain model for the system, some impossible scenarios are excluded from the formal analysis, which means that the formal analysis is simplified. This thesis presents a domain model for railway control systems, expressing constraints on how trains can behave in a railway network. The railway network is abstracted into a simple graph structure and the model is described in a temporal predicate logic using operators for the initial (I) and the next (X) value. The model is carefully defined in order not to introduce any unrealistic behavior.