Formal Analysis For Train Control System Based On Runtime Verification

Railway system is one of the most important part of railway system, it is the main factor affects the safety of train system. With the rapid development of computer technology, the safety assurance methods test, which is widely used in railway field could no longer satisfy the ever increasing safety demand of complex computer system because it is an incomplete method. Model checking is a complete method, but it has the problem of the contradiction between model expression and verification ability. Runtime verification has emerged as a light-weight formal verification technique that bridges the gap between traditional testing and model checking.In this thesis, we present a 4-valued executable semantics for finite trace LTL, to deal with the un-accurate problem of the detect results in traditional LTL semantics with the extension of the value set true and false with presumably true and presumably false. Then we present the syntax and semantics of past time based 4-valued LTL, which could improve verification efficiency when analyzing fault states. Meanwhile, we present the algorithm of negative approximation to improve verification efficiency. To make runtime verification can be used to analyze the log files of systems, we develop a tool named Runtime Verification tool. Finally, we use runtime verification in railway field with the verification of two important scenario:communication initiation process and RBC handover.