原文传递
基于TCSP的区域控制器分层建模与验证
| 论文题名： | 基于TCSP的区域控制器分层建模与验证 |
| 关键词： | 城市轨道交通;列车自动控制系统;区域控制器;分层建模 |
| 摘要： | 城市轨道交通是解决大城市拥堵、方便百姓出行的重要手段之一。基于通信的列车自动控制系统CBTC(Communication Based Train Control)是保证城市轨道交通行车安全、高效运营的系统，区域控制器ZC(Zone Controller)作为CBTC系统的关键设备，具有实现列车管理、移动授权计算等安全功能。本文针对ZC子系统功能的安全验证，传统仿真、测试的方法存在操作量大、完备性不强，单一形式化方法难以描述ZC子系统复杂功能的问题，给出了一种基于TCSP(TimedCommunicating Sequential Process)的分层建模与验证方法来对ZC子系统安全性验证进行了研究。 本文采用的分层建模方法是将ZC子系统分为系统层和功能层，层间靠系统数据关联，并采用加入时间机制的建模方法来表达系统的实时性，用UML-RT(Unified Modeling Language-Real Time)顺序图形象直观的描述系统交互层，利用标签迁移系统LTS(Labelled Transition System)，实现半形式化UML-RT到形式化语言TCSP的转换，结合内部功能处理层的TCSP模型，建立整体的基于TCSP的ZC子系统分层模型，层次清晰、要素明确。在现有的通信顺序进程验证软件PAT(Process Analysis Toolkit)上运行，基于LTL(Linear Temporal Logic)断言对技术规范提出的数据相关需求进行验证。 论文选取任务启动及正常行车场景案例进行分析。车地交互系统每个周期根据系统输入和控制规则得到移动授权MA(Movement Authority)，在没有故障和突发事件的情况下，下个周期依照相同的规则得到对应MA信息，若有回撤现象发生，不符合安全条件。根据跳变故障迹找到系统存在的问题并给出解决方案，使ZC子系统满足需求规范相关要求，最大限度的避免系统设计可能的缺陷和错误，确保ZC子系统功能的正确性，对进一步提高ZC子系统安全性有重要意义。 |
| 作者： | 张淼 |
| 专业： | 交通信息工程及控制 |
| 导师： | 黄友能 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2015 |
| 正文语种： | 中文 |
检索历史
应用推荐
