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

摘要：

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

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

所属期刊栏目：33

分类号：U284.482(铁路通信、信号)

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

在线出版日期：2012-04-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：65-71