基于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验证器当中完成对计算机联锁系统模型的验证工作。验证结果表明:该方法能够实现高效准确地验证联锁系统需求的正确性，且能够举出反例从而修正可能出现的错误，为计算机联锁系统需求模型的正确性验证提供一种新思路。

目录

声明

摘要

1 绪论

1．1 论文的选题背景和研究意义

1．2 国内外研究现状

1．2．1 国内研究现状

1．2．2 国外研究现状

1．2．3 研究现状分析

1．3 论文结构和主要研究内容

1．4 小结

2 UML及形式化方法

2．1 UML统一建模语言

2．1．2 UML的语义

2．2 形式化方法概述

2．3 符号模型检测NuSMV

2．3．1 NuSMV简介

2．3．2 NuSMV的系统描述

2．3．3 NuSMV的语义结构

2．4 小结

3 计算机联锁系统的UML模型

3．1 计算机联锁系统的需求分析

3．1．1 计算机联锁系统框架

3．1．2 进路控制过程分析

3．2 计算机联锁系统UML模型的建立

3．2．1 UML用例图的建立

3．2．2 联锁系统受控对象UML类图与状态图的建立

3．2．3 进路控制过程UML顺序图与状态图的建立

3．3 进路搜索过程的UML模型

3．3．1 基于坐标与站场拓扑的进路搜索算法

3．3．2 进路搜索UML模型的建立

3．4 小结

4 UML模型到NuSMV模型的转换

4．1 转换规则的建立与实现

4．1．1 类图的转换

4．1．2 状态图的转换

4．1．3 顺序图的转换

4．2 模型转换程序的设计

4．2．2 基于C#的UML到NuSMV模型转换程序的设计

4．3 小结

5 计算机联锁系统的NuSMV形式化验证

5．1 NuSMV模型的验证

5．2 联锁系统验证语句分析

5．2．1 形式化系统模型的相关性质

5．2．2 待验证性质的提取与表达

5．3 验证的过程与结果分析

5．3．1 模型的验证过程

5．3．2 进路控制过程的验证结果与分析

5．4 小结

结论

致谢

参考文献

攻读学位期间的研究成果