基于运行时验证的列控系统形式分析

论文摘要

列车运行控制系统是轨道交通信号系统的重要组成部分之一,是保证列车运行安全的主要因素之一。随着计算机技术在列车运行控制系统中的应用,安全问题显得越发的重要和复杂,传统的测试方法由于其不完备性难以满足以计算机技术为基础的安全系统的需要。模型检验是一种完备的验证系统的方法,但是会遇到模型刻画能力与验证能力矛盾的问题。运行时验证是一种将模型检验方法与测试相结合的轻量级形式化验证方法,它能够有效地降低系统验证的复杂度,提供系统运行阶段的安全保障。本文提出了一种基于4真值逻辑的LTL（线性时序逻辑）可执行语义,该语义在逻辑真值“真”和“假”基础上增加了逻辑值“可能真”和“可能假”,以解决传统LTL语义判定结果不准确问题。之后本文提出了基于过去时态的4真值LTL语法及语义,可提高故障状态分析效率。本文还提出了公式的负近似计算方法,可在不削弱公式发现错误轨迹的同时提高验证效率。为了使运行时验证更加便于进行系统日志文件分析,本文开发了运行时验证工具Runtime Verification tool,并通过验证CTCS-3级列控系统的两个重要场景：通信会晤建立及RBC交接说明运行时验证在列控领域的应用方法。

论文目录

• 致谢
• 摘要
• ABSTRACT
• 1 引言
• 1.1 选题的目的及意义
• 1.2 CTCS-3级列车运行控制系统介绍
• 1.3 形式化方法研究现状
• 1.4 本文研究内容及组织结构
• 1.5 本章小结
• 2 运行时验证的理论基础
• 2.1 运行时验证特点
• 2.1.1 传统验证方法的不足
• 2.1.2 运行时验证的特点
• 2.2 运行时验证方法
• 2.3 线性时序逻辑LTL
• 2.3.1 基于有限序列的LTL语法
• 2.3.2 基于有限序列的LTL语义
• 2.4 本章小结
• 3 基于4真值LTL的运行时验证
• 3.1 4真值LTL的语法及语义
• 3.1.1 基于将来时态的LTL语义
• 3.1.2 基于过去时态的LTL的语法及语义
• 3.2 基于4真值LTL的公式重写算法
• 3.2.1 基于4真值将来时态LTL的重写逻辑算法
• 3.2.2 基于4真值过去时态LTL的重写逻辑算法
• 3.3 运行时验证在Maude中的实现
• 3.4 公式近似算法
• 3.5 本章小结
• 4 案例分析
• 4.1 运行时验证工具开发
• 4.2 CTCS-3车地通信会晤建立的运行时验证
• 4.2.1 车地通信会晤建立过程
• 4.2.2 车地通信会晤建立过程的验证
• 4.3 CTCS-3中RBC交接过程的运行时验证
• 4.3.1 RBC交接过程
• 4.3.2 RBC交接过程的验证
• 4.4 本章小结
• 5 结论
• 参考文献
• 表目录
• 图目录
• 作者简历
• 学位论文数据集