运行时验证及其在列车运行控制系统中的应用

Runtime Verification and its Applications in Train Control Systems

运行时验证是一种将模型检验方法与测试相结合的轻量级验证技术,它能够有效地降低系统验证的复杂度,提供系统运行阶段的安全保障,因此在安全苛求系统的验证领域有着极其重要的应用。本文提出一种基于三值逻辑的有限轨迹LTL可执行语义,允许"真"和"假"以外的逻辑值来显式的刻画验证过程中可能出现的非确定性,从而使得验证的结果更加精确。针对新的LTL语义给出了基于公式重写的运行监控算法和近似优化策略,并结合欧洲列车运行控制系统的实例,分析探讨了该方法在轨道交通控制领域的应用。

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.