原文传递
基于公式重写的实时时序约束验证及其在列控背景下的应用
| 论文题名： | 基于公式重写的实时时序约束验证及其在列控背景下的应用 |
| 关键词： | 轨道交通信号;列控系统;时序约束;公式重写规则 |
| 摘要： | 列控系统是一类安全苛求系统，是轨道交通信号系统的核心部分，需要采取各种技术手段确保系统设计和运行的正确性，而运行时验证就是众多对列控系统进行安全验证的手段之一。它结合了模型检验和传统测试的特点，降低了系统验证的复杂度。运行时验证将系统在实际运行时的行为特性作为研究对象，主要研究由实际采集到的运行信息组成的有限长度执行轨迹是否满足系统的设计和安全规范。目前运行时验证领域主要使用线性时序逻辑LTL来描述系统规范中的时序约束，即先后发生的事情在时间上的约束关系。但LTL所研究的对象即由离散时间点组成的系统执行轨迹并未考虑系统的真实执行时间，因此LTL往往难以表达涉及精确实时属性的时序约束。 通过构造基于与系统真实时间同步的离散时间点组成的系统执行序列，RTLTL可以刻画具有精确实时属性的时序约束，从而克服了LTL难以表达此类约束的缺陷。在这个基础上本文提出了基于公式重写的RTLTL监控算法，并以此在验证工具Maude中实现了对由RTLTL公式表达的实时时序约束的一般运行时验证。但是这种验证在执行方式上并未考虑执行轨迹随时间流逝长度增大的情况，灵活性较差，而且经过实验发现在处理大规模轨迹时效率也有问题。为了解决这些问题，本文提出了一种基于Maude交互式扩展IMaude的增量式运行时验证方法并开发了相应辅助软件工具框架。本文主要工作包括(1)提出了基于重写逻辑的RTLTL约束监控算法，并在重写工具Maude中实现了相应运行时验证。(2)提出了一种基于IMaude交互式重写的增量式运行时验证方法。(3)对列控背景下两个具有实时时序约束的具体案例进行了方法的应用，验证了方法的有效性。 |
| 作者： | 李旸 |
| 专业： | 控制工程 |
| 导师： | 赵林 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2015 |
| 正文语种： | 中文 |
检索历史
应用推荐
