SAT-based Model Checking and its applications to Train Control Software
Phillip James · 2010
Formal verification of railway control software has been identified to be one of the “grand challenges” [Jac04] of Computer Science. In this thesis, we demonstrate the successful application of various SAT-based model checking techniques to verify train control systems. Starting with a propositional model for a control system, more specifically an interlocking, we show how execution of the system can be modelled via a finite automaton. We give both bounded and unbounded algorithms to perform SAT-based model checking over such an automaton, commenting on the advantages and disadvantages of each. In order to tackle the state space explosion problem, we propose slicing. We then give the correctness of this method with respect to our modelling approach. The result of the thesis is a verification tool that combines the algorithms considered within the thesis. The tool has been applied to two real world interlocking systems and a discussion of the results is given.