论文部分内容阅读
CTCS(China Train Control System,中国列车运行控制系统)是保证我国铁路列车安全运行的关键技术装备,其中,CTCS-3级列控系统首次结合了GSM-R和轨道电路两种车地传输方式,兼容了CTCS-2级列控系统作为其后备系统,在CTCS-3级系统出现故障或者列车进入CTCS-2级区段时,需要进行等级转换,转换的成功与否直接关系到列车的运行安全和行车效率。因此,对等级转换场景的研究很有必要。CTCS-3级列控系统的需求规范是对系统进行研究和开发的基础资料,对其进行建模和验证可以有效的发现系统缺陷。在对系统进行建模和验证的过程中,最重要的是要保证系统和模型的一致性。UML(Unified Modeling Language,统一建模语言)在开发研究人员中有着广泛的应用基础,图形表达简易多样,可以细致全面的表达系统模型,然而它不具备严格的数学定义,对模型的验证较为逊色。形式化方法可以有效的解决模型验证问题,但其逻辑表达方式复杂,直接用其建模势必会对模型与系统的一致性带来困难。本文通过将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的转换规则,将等级转换系统转换为具有严格数学语义的形式化模型并加以验证,为其他复杂系统的形式化建模与验证提供了参考方法。