Runtime Verification and its Applications in Train Control Systems
Xian Li · Journal of the China Railway Society · 2011
Runtime verification has emerged as a promising verification technique that bridges the gap between traditional testing and model checking.It supplements formal verification with more lightweight dynamic techniques when these techniques fail due to complexity of issues,and it has important applications in the field of safety critical systems verification.In this paper,we present a 3-valued executable semantics for finite trace LTL,which can express the uncertainty during the monitoring proces by allowing additional truth values in the logic.The rewriting based monitoring algorithm and a novel approximation technique for the new semantics are proposed,and demonstrated by a use case from the European Train Control System.