Safety Monitoring for ETCS with 4-valued LTL

When verifying the safety of ETCS, testing and formal methods have limitations to some degree. Runtime verification is effective to detect deviation between the current and the expected system behaviors. To improve the accuracy of runtime monitoring, 4-valued LTL (Linear Time Logic) semantics and formula rewriting based algorithm are proposed. Furthermore, approximation technique is presented for 4-valued LTL formulae to make the verification procedure high efficient. Finally, the method is applied to the European Train Control System (ETCS) by monitoring several scenario traces. The experimental results show that the 4-valued LTL semantics are able to generate the most accurate verification outcomes. It can also be found that the approximation technique improves the verification efficiency apparently in some cases.