论文部分内容阅读
随着我国经济的快速发展，铁路的发展已经步入黄金期。目前我国线路大多使用CTCS-3（Chinese Train Control System，中国列车运行控制系统）级列车运行控制系统，等级转换场景作为CTCS-3级列控系统的主要场景之一，在确保车载设备正常转换及故障转换中扮演着非常重要的角色。CTCS-3级列控系统需求规范作为系统开发的前提，描述了等级转换场景所必备的相关功能需求及性能要求，系统进行等级转换的成功与否直接影响到列车的运行安全和行车效率，等级转换时间长短以及列车运行速度的大小对保障系统的安全具有重要意义。因此，以等级转换场景作为研究对象，形式化建模方法为出发点，列控系统的需求规范为准则，对其等级转换场景进行形式化建模与验证很有必要。 对系统进行建模验证的关键是保证系统与模型的一致性。UML(Unified ModelingLanguage，统一建模语言)在开发研究人员中有着广泛的应用基础，图形表达简易多样，对模型可进行细致全面的描述，但其缺乏模型验证。形式化建模可有效解决模型验证，由于其逻辑表达复杂，单独用其建模会对模型与系统的一致性带来困难。本文通过UML与有色Petri网理论相结合的方式进行等级转换场景的形式化建模。首先，通过对系统需求规范的总结，对正常情况下的两种等级转换场景进行描述。其次，分别建立两种转换方式下CTCS-2级向CTCS-3级转换、CTCS-3级向CTCS-2级转换的UML模型，实现对转换场景的消息交互过程及静态转化过程的描述。根据系统的需求规范，分析等级转换场景的性能及功能需求，制定由UML模型向有色Petri网模型的转换规则，将建立的等级转换场景UML模型转换为有色Petri网模型，利用验证工具CPN Tools对通过转换所得到的模型进行仿真验证，验证了模型结构和逻辑的正确性，从而达到对模型与系统一致性的目的。最后，通过对建立模型的模拟运行，将提取的运行数据进行MATLAB仿真，得到了列车运行速度与转换时间和转换成功率的关系，并讨论了影响等级转换稳定性的因素。结果表明，根据文章提供的方法建立的有色Petri网模型可以满足系统的性能要求，为其他复杂系统的形式化建模与验证提供了参考方法。