原文传递
基于时间自动机的ZC子系统建模与验证
| 论文题名： | 基于时间自动机的ZC子系统建模与验证 |
| 关键词： | 列车运行控制;区域控制器;时间自动机;逻辑性;时序性 |
| 摘要： | 近年来，随着城市化进程的加速，城市轨道交通迅速发展，基于通信的列车运行控制（Communication Based Train Control，CBTC）系统逐渐被广泛使用。区域控制器(Zone Controller，ZC)作为CBTC系统地面核心子系统，通过与其它设备间的交互通信，实时的为列车计算移动授权(Movement Authority，MA)信息，实现列车的间隔控制。ZC子系统作为一个典型的实时系统，其行为状态的迁移过程中，逻辑性和时序性的正确对保障系统安全具有重要意义。因此，为了进一步确保ZC子系统能够安全运行实现其功能，本文提出了一种基于时间自动机的ZC子系统建模与验证方法，通过对系统进行建模，从逻辑性和时序性两方面验证分析系统运行时是否满足安全需求。 本文首先对ZC子系统的特点进行了分析，并采用层次化结构思想把ZC子系统分为系统设备层和功能逻辑层。其次，根据UML扩展方式，针对ZC子系统特点，把顺序图元模型在时钟约束和变量两方面做了合理扩展，使其能够更充分地描述系统在交互过程中的逻辑性和时序性。然后，根据模型转化理论，在确保模型转换过程一致性的基础上，制定合理的转换规则，把半形式化扩展顺序图转化为形式化的时间自动机模型。并对形式化验证方法分类做了概述，阐述了时间自动机模型验证工具UPPAAL的基本结构和功能。在此基础上，分析了LTL公式到BNF公式的逻辑语义转换形式。 本文最后选取MA回撤和列车跨越ZC边界区域两个场景案例进行分析，分别建立时间自动机模型，并在UPPAAL软件中构造了时间自动机网络模型。通过对两个不同场景下系统需求的逻辑性和时序性验证，从逻辑性和时序性方面保证了系统的安全运行。证明了本文提出的建模和验证方法的可行性和有效性。 |
| 作者： | 张鹏基 |
| 专业： | 交通信息工程及控制 |
| 导师： | 黄友能 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2017 |
| 正文语种： | 中文 |
检索历史
应用推荐
