基于uml和uppaal的ctcs-3级列控系统等级转换场景建模与验证

《基于uml和uppaal的ctcs-3级列控系统等级转换场景建模与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、ＩＷ９４５．１２公开：密备；中图分类号ＵＤＣ：号：本校编續Ｗ义遠乂＃工程硕±学位论文ＵＭＬＵＰＰＡＡＬＣＴＣＳ－基于和的３级论文题目＝列控系统等级转换场景建模与验证研究生挂名：胡雪蓮学号：０６１２０５２学校指导教师姓名：岡彩霞职称：教授企业指导教师姓名文雨高级工程师：曹职称：交通运输工程申请学位工程领域名称：２Ｄ１５，６，１２２０１５．６．９论文提交日期：论义答辩日期：独创性声明本人声明所呈交的学位论文是本人在导师指导下进斤的研究工作和取得的研究成果，除了文中特别加Ｗ标注和致谢之处

2、外，论文中不包含其他人已经发表或撰写过的研究成果。，也不包含获得兰州巧通大学或其他教育机构的学位或证书而使用过的材料与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。、学位论文作者签名：毛同雪蓋日期：年＾月ａ日＿签字学位论文版权使用授权书本学位论文作者完全了解兰州交通大学有关保留、使用学位论文的规定。特授权１＾将学位论文的全部或部分内容编入有关数据库进行检索兰州交通大学可，并采用影印、缩印或扫描等复制手段保存、汇编供查阅和借阅。同意学校向国家有关部口或机构送交论文的复印件和磁盘。（保密的学位论文在解密后适用本

3、授权说明）！建学位论文作者签名：社１雪导师签名：（作憂ＩＸ签字円期：年（月円签字曰期：年（月序曰工程硕士学位论文基于UML和UPPAAL的CTCS-3级列控系统等级转换场景建模与验证ModelingandVerificationofLevelTransitionSceneinCTCS-3LevelTrainControlSystemBasedonUMLandUPPAAL作者姓名：胡雪莲工程领域：交通运输工程研究方向：列控系统建模与验证学号：0612052校内导师：陶彩霞教授企业导师：曹文雨高级工程师完成日期：2015年4月18日兰州交通大学LanzhouJiaoton

4、gUniversity兰州交通大学工程硕士学位论文摘要CTCS(ChinaTrainControlSystem,中国列车运行控制系统)是保证我国铁路列车安全运行的关键技术装备，其中，CTCS-3级列控系统首次结合了GSM-R和轨道电路两种车地传输方式，兼容了CTCS-2级列控系统作为其后备系统，在CTCS-3级系统出现故障或者列车进入CTCS-2级区段时，需要进行等级转换，转换的成功与否直接关系到列车的运行安全和行车效率。因此，对等级转换场景的研究很有必要。CTCS-3级列控系统的需求规范是对系统进行研究和开发的基础资料，对其进行建模和验证可以有效的发现系统缺陷。在对系统进行建模和

5、验证的过程中，最重要的是要保证系统和模型的一致性。UML(UnifiedModelingLanguage,统一建模语言)在开发研究人员中有着广泛的应用基础，图形表达简易多样，可以细致全面的表达系统模型，然而它不具备严格的数学定义，对模型的验证较为逊色。形式化方法可以有效的解决模型验证问题，但其逻辑表达方式复杂，直接用其建模势必会对模型与系统的一致性带来困难。本文通过将UML与时间自动机理论相结合的方式，先用UML全面的刻画系统，然后制定详细的转换规则，将UML模型转换为时间自动机模型，并利用其验证工具UPPAAL加以验证，来达到对CTCS-3级列控系统等级转换场景验证的目的。本文首

6、先对CTCS-3中等级转换场景的需求规范做了归纳总结，提取出系统的性能要求。其次对转换场景的两种转换方式，CTCS-2级向CTCS-3级转换和CTCS-3级向CTCS-2级转换，分别建立了消息顺序图，UML时序图和UML状态图模型，以达到所建模型和系统一致性的目的。然后根据UML时序图和UPPAAL模型图的共同点，制定了从消息顺序图到UML时序图，再从UML时序图结合UML状态图转换为UPPAAL模型图的转换规则，并根据转换规则，得出了两种等级转换方式下的UPPAAL模型图。最后，利用验证工具UPPAAL对通过转换所得到的模型进行仿真验证，结果表明根据文章提供的方法建立的UPPAA

7、L模型可以满足系统的性能要求。本文为了达到系统与模型一致性的目的，制定了从UML到UPPAAL的转换规则，将等级转换系统转换为具有严格数学语义的形式化模型并加以验证，为其他复杂系统的形式化建模与验证提供了参考方法。关键词：CTCS；等级转换；UML；UPPAAL；建模论文类型：应用研究-I-基于UML和UPPAAL的CTCS-3级列控系统等级转换场景建模与验证AbstractChinaTrainControlSystem(CTCS)isthekeytechnology