基于UML的列控系统建模方法与验证工具集成

摘要

近年来随着技术的发展，列车运行控制系统的功能不断增强，为实现不同厂商设备间、地面设备与车载设备间互联互通，使列车能够在轨道交通网中跨线安全运行，列控系统需求规范的作用正日益突显。但现有研究成果表明在需求层面对系统的关键属性进行分析和确认面临很多困难，需要提出一种合理的框架结构以对其关键属性进行建模并对系统进行验证。
　　从建模方法来看，统一建模语言(UML)具有定义良好、易于表达、描述直观等优点，已被广泛应用到不同的领域，但当需要对影响列车安全可靠运行的连续和离散过程进行一体化建模时，对混成特性的描述已远远超出了这种建模语言本身的能力范围，这给列控系统需求规范的建模工作带来了巨大的挑战。
　　从验证方法来看，形式化方法已成为保障安全苛求系统的安全性与可靠性的重要手段。针对不同的系统、同一系统的不同性质和系统分析的不同阶段，可供研究人员使用的形式化验证工具种类繁多。
　　因此，本文从列控系统需求规范建模方法与验证工具集成着手进行研究，主要内容包括：
　　1.对列控系统需求规范混成特性建模需求进行分析，研究UML扩展机制，充分挖掘UML的图形功能，设计面向列控系统需求规范的混成UML概要文件，使之能够包含更多的内容与信息去准确地刻画列控系统的混成特性。
　　2.在论述列控系统需求规范的分析方法体系结构的基础上，重点分析了模型验证阶段的功能需求。在Eclipse平台上完成了验证支持工具的软件原型开发，对底层形式化建模过程和验证工具进行封装，通过自动化的模型检验技术来寻找需求中隐藏的错误，使现有的需求管理工具(IBM RequisitePro)、建模工具(IBMRational Software Architect)和验证工具(NuSMV，PHAVer)实现高度集成，并具备良好的可扩展性。并给出从UML模型到形式化模型的转换规则，构造了面向对象语言UML以及NuSMV、PHAVer形式化语言之间的转换桥梁。
　　3.从列控系统需求规范中选取了具有代表性的模式转换场景和RBC交接场景，利用所提出的混成UML概要文件对场景进行建模；将建好的模式转换场景模型转换为NuSMV模型，而将RBC交接场景模型转换为PHAVer模型；在开发的验证支持工具中完成两个形式化模型的验证分析工作。通过案例分析，证明文中所提出的基于UML扩展机制的列控系统需求规范建模方法的可行性，以及所开发验证支持工具的可用性。