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