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

Runtime Verification and its Applications in Train Control Systems

作　　者：赵林[1] 唐涛[1] 徐田华[1] 柴铭[1] 李宪[1] 

机构地区：[1]北京交通大学轨道交通控制与安全国家重点实验室,北京100044

出　　处：《铁道学报》2011年第12期65-71,共7页Journal of the China Railway Society

基　　金：国家重点实验室自主课题基金(RCS2008ZQ002;RCS2008ZZ005);中央高校基本科研业务费专项基金(2011JBM322);北京交通大学-泰雷兹集团国际合作项目(M&V-SCHS)

摘　　要：运行时验证是一种将模型检验方法与测试相结合的轻量级验证技术,它能够有效地降低系统验证的复杂度,提供系统运行阶段的安全保障,因此在安全苛求系统的验证领域有着极其重要的应用。本文提出一种基于三值逻辑的有限轨迹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.

关 键 词：模型检验 测试 多值逻辑 公式重写 列车运行控制系统 

分 类 号：U284.482[交通运输工程—交通信息工程及控制]