Improving formal analysis of computerised rail traffic control systems using domain models
Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
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.
Place, publisher, year, edition, pages
2016. , 37 p.
Engineering and Technology
IdentifiersURN: urn:nbn:se:uu:diva-283398OAI: oai:DiVA.org:uu-283398DiVA: diva2:919000
Bachelor Programme in Computer Science
Eriksson, Lars-HenrikGällmo, Olle