原文传递
基于UML-NuSMV的联锁软件形式化建模与验证
| 论文题名： | 基于UML-NuSMV的联锁软件形式化建模与验证 |
| 关键词： | 铁路信号;计算机联锁系统;形式化验证;UML模型;NuSMV模型;自动转换 |
| 摘要： | 计算机联锁系统是铁路控制的核心系统之一，是保障铁路运输安全的重要一环。作为典型的安全苛求系统，计算机联锁软件的设计与开发应严格地按照相关规定和高行业标准进行。随着铁路系统的快速发展，在联锁软件开发的需求分析阶段通过形式化的验证找出存在的问题，对保证铁路运输系统的安全高效运行有着重要意义。然而直接采用形式化方法有着对专业知识要求高、使用难度大和建模效率低下等缺点，因此在站场的规模与复杂度不断提高的今天，需要开发一种更加高效便捷的联锁软件形式化验证方法用以保障其正确性。 UML(Unified Modeling Language，统一建模语言)如今被广泛应用于软件开发领域的各个阶段，它通过多个视图结合能够准确全面地从不同角度描述一个系统，然而其作为一种半形式化的语言不能提供有效的自动分析与验证方法。NuSMV(New SymbolicModel Verifier，符号模型验证器)是一种高效成熟的形式化验证工具，若能够通过UML建立联锁系统模型，再将之转化为形式化的NuSMV模型并对其进行验证，则可以通过间接的方式实现降低对联锁系统形式化建模与验证的难度与提高效率的目的。 针对上述问题，本文提出一种UML与NuSMV相结合的计算机联锁系统形式化验证的方法。首先分析联锁系统的框架结构与进路控制中每一阶段的需求，并针对进路选择阶段提出了一种基于坐标与站场拓扑的进路搜索算法，以一个标准站场为例利用UML类图、状态图与顺序图这三种视图建立联锁控制逻辑的需求模型。其次分析对比UML模型与NuSMV形式化模型在结构和语义上的关联，并结合设备间相互制约的特点制定了一套UML模型到NuSMV模型的转换规则。然后根据此规则在C＃环境下编写了相应的模型转换程序，完成了UML模型到NuSMV模型的批量自动转换。最后，分析与提取计算机联锁系统需遵循的相关技术规范，应用CTL(Computation Tree Logic，计算树逻辑)表达式描述联锁模型应满足的一些性质，并将其作为验证语句输入至NuSMV验证器当中完成对计算机联锁系统模型的验证工作。验证结果表明:该方法能够实现高效准确地验证联锁系统需求的正确性，且能够举出反例从而修正可能出现的错误，为计算机联锁系统需求模型的正确性验证提供一种新思路。 |
| 作者： | 刘征 |
| 专业： | 交通信息工程及控制 |
| 导师： | 武晓春 |
| 授予学位： | 硕士 |
| 授予学位单位： | 兰州交通大学 |
| 学位年度： | 2018 |
| 正文语种： | 中文 |
检索历史
应用推荐
