原文传递
基于UML和UPPAAL的CTCS-3级列控系统等级转换场景建模与验证
| 论文题名： | 基于UML和UPPAAL的CTCS-3级列控系统等级转换场景建模与验证 |
| 关键词： | 列车运行控制;统一建模语言;转换场景;安全运行 |
| 摘要： | CTCS(中国列车运行控制系统)是保证我国铁路列车安全运行的关键技术装备，其中，CTCS-3级列控系统首次结合了GSM-R和轨道电路两种车地传输方式，兼容了CTCS-2级列控系统作为其后备系统，在CTCS-3级系统出现故障或者列车进入CTCS-2级区段时，需要进行等级转换，转换的成功与否直接关系到列车的运行安全和行车效率。因此，对等级转换场景的研究很有必要。CTCS-3级列控系统的需求规范是对系统进行研究和开发的基础资料，对其进行建模和验证可以有效的发现系统缺陷。 在对系统进行建模和验证的过程中，最重要的是要保证系统和模型的一致性。UML(统一建模语言)在开发研究人员中有着广泛的应用基础，图形表达简易多样，可以细致全面的表达系统模型，然而它不具备严格的数学定义，对模型的验证较为逊色。形式化方法可以有效的解决模型验证问题，但其逻辑表达方式复杂，直接用其建模势必会对模型与系统的一致性带来困难。本文通过将UML与时间自动机理论相结合的方式，先用UML全面的刻画系统，然后制定详细的转换规则，将UML模型转换为时间自动机模型，并利用其验证工具 UPPAAL加以验证，来达到对CTCS-3级列控系统等级转换场景验证的目的。 本文首先对CTCS-3中等级转换场景的需求规范做了归纳总结，提取出系统的性能要求。其次对转换场景的两种转换方式，CTCS-2级向 CTCS-3级转换和CTCS-3级向CTCS-2级转换，分别建立了消息顺序图，UML时序图和UML状态图模型，以达到所建模型和系统一致性的目的。然后根据UML时序图和UPPAAL模型图的共同点，制定了从消息顺序图到UML时序图，再从UML时序图结合UML状态图转换为UPPAAL模型图的转换规则，并根据转换规则，得出了两种等级转换方式下的UPPAAL模型图。最后，利用验证工具 UPPAAL对通过转换所得到的模型进行仿真验证，结果表明根据文章提供的方法建立的UPPAAL模型可以满足系统的性能要求。 本文为了达到系统与模型一致性的目的，制定了从UML到UPPAAL的转换规则，将等级转换系统转换为具有严格数学语义的形式化模型并加以验证，为其他复杂系统的形式化建模与验证提供了参考方法。 |
| 作者： | 胡雪莲 |
| 专业： | 交通运输工程 |
| 导师： | 陶彩霞;曹文雨 |
| 授予学位： | 硕士 |
| 授予学位单位： | 兰州交通大学 |
| 学位年度： | 2015 |
| 正文语种： | 中文 |
检索历史
应用推荐
