原文传递
面向列控安全性监控的运行时验证方法研究
| 论文题名： | 面向列控安全性监控的运行时验证方法研究 |
| 关键词： | 列车控制系统;运行时验证;安全监控;线性时序逻辑;无线闭塞 |
| 摘要： | 列车控制系统是轨道交通信号系统的重要组成部分之一，是保证列车运行安全的重要部分，测试与形式验证是确保其安全性的主要途径。传统的测试方式由于其不完备性，难以测试可能的运行环境与路径，因此无法保证运行后的系统不存在安全缺陷；模型检验是一种完备的验证系统的方法，但是会遇到模型刻画能力与验证能力矛盾的问题，尤其是状态爆炸问题会使得该方法对于复杂系统难以适用。运行时验证是一种轻量级的验证技术，其验证过程伴随目标系统的实际运行，对系统运行路径是否满足安全性质进行及时监控，是传统测试和验证技术的有效补充，在许多领域逐渐受到人们的关注，并被具体运用到众多对系统安全性有着较高要求的行业。 本文针对列控系统中分路不良、无线闭塞中心RBC切换等对列控安全极其重要的问题入手，研究相应的运行时验证技术，包括： （1）分析轨道电路子系统中分路不良场景及其发生的原因，总结了对分路不良进行监控以保证列车安全性的一组关键性质，并提出用线性时序逻辑（LTL）描述和生成监控器的方法。由于分路不良问题需要多个监控监控器同时监控，为了提高监控效率，还提出了了针对分路不良的多监控器调度策略。 （2）为了实现监控性质的辅助描述和自动生成，本文针对列控系统安全性监控需要考虑的主要特征，包括监控事件的描述、非插装式的监控器运行机制、列控系统主要采用C语言等，对JavaMOP监控工具进行扩展，对其MOP文件格式重新设计，扩展了事件与条件定义语言，并实现了相应的监控器生成工具。 （3）为了验证上述方法和工具的有效性，对列控系统中无线闭塞中心RBC子系统的RBC切换场景进行了实验分析，对RBC切换交接过程中必须满足的安全性质进行规约并生成相应的监控器，以及时发现危险情况，取得了良好效果，从而验证了上述方法的适用性以及原型工具的有效性。 |
| 作者： | 徐蛟 |
| 专业： | 软件工程 |
| 导师： | 董威 |
| 授予学位： | 硕士 |
| 授予学位单位： | 国防科学技术大学 |
| 学位年度： | 2014 |
| 正文语种： | 中文 |
检索历史
应用推荐
