论文部分内容阅读
CTCS-3是我国列车运行控制系统中现行的最高应用等级,是一种基于GSM-R的在地面与列车之间连续、双向信息无线传输实时系统。在国产化列车运行控制系统的进程中,研究并验证CTCS-3技术规范是保障列车安全、快速、高效地运行的重要组成部分。实时系统中微小的逻辑错误都能导致不可预见的灾难性后果,所以对CTCS-3规范建模验证无疑将是有效的手段,然而面临的问题是如何保证在对实时系统一致性建模的前提下对模型做具有完备性的模型验证。保障模型和系统的一致性是实现规范验证的第一步。模型不仅要能够准确细致地对实时系统刻画,还必须在开发人员中具有广泛的应用基础。UML满足上述模型要求,然而它不具有模型验证的能力。形式化模型检验在仿真验证方面有着无可比拟的优势,但是利用形式化语言直接将文字形式的系统规范转化成模型实属不易。如果能够架起上述两种模型的桥梁,将UML模型无差的转化成形式化模型并加以验证,就能够保证在准确复现系统的前提下对规范进行仿真验证。本文选择了时间自动机模型作为形式化建模手段,辅以UPPAAL模型验证工具。本文首先对CTCS-3中RBC切换场景分析并对UML针对实时系统做扩展,利用扩展了的UML按照RBC切换过程中几个关键事件集分别建模得到相应子顺序图,将子顺序图整合继而得到完整的过程顺序图。之所以对过程按事件集分别建模是为了方便后文中转化时间自动机模型。在遵循时间自动机模型相关语义并且结合列控系统特点的基础上,将UML子顺序图转化成对应的时间自动机子模型,然后按照相同状态集合并的原则得到完整的时间自动机模型。本文在转化过程中制定了一般规则。将独立的时间自动机模型组成时间自动机网络模型。利用UPPAAL对既得模型仿真得到仿真迁移图,利用从文字规范中提炼的BNF语句对模型的死锁、系统功能做完备的形式化验证,从而达到对规范研究并验证的目的。UML模型和UPPAAL时间自动机网络模型的结合在规范语义的准确表达与模型验证上达到了高度统一,为CTCS-3列控系统的研究提供参考。