基于UML-NuSMV的联锁软件形式化建模与验证

发布时间：2020-05-15 14:35

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

- 7 -图 2.1 UML 模型的构成示意图L 模型图构成的内容分为以下三项：事物成实际系统的主要内容进行抽象，是构成 UML 模型的基本单元。UML 中物：构建事物用于描述模型的静态基本元素或概念，如类与接口等；行为当中事物间的交互与事物自身的状态转变这一类动态部分；分组事物划分构；注释事物负责对模型中内容的解释。关系事物之间存在何种关联，关系的类型有如下四种：依赖：对于一个独立的事物而言，若它的状态发生变化，则依赖于它的相样变化。

基于UML-NuSMV 的联锁软件形式化建模与验证一种有效的解决方案。检测是一种基于时态逻辑的形式化验证方法，验证系统时其核心的关时态性质的变化。基于模型检测方法的主要内容分为三个部分，，如图建立系统 S 的抽象模型 M，通过一种特定的数学语言逻辑对系统 S 的模式进行描述；第二步是建立性质规约，即根据系统 S 应完成的功能过公式对其进行表达，使其成为系统的约束性质ψ；第三步是形式化模型M进行状态空间的检测，验证其在所有状态中是否都能够满足约M|=ψ，若模型中存在不能满足该约束性质的状态，则将其列出以供修
【学位授予单位】：兰州交通大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：U284.362

【相似文献】

相关期刊论文 前10条

1 张树群;;车站计算机联锁系统设备及其使用[J];郑铁科技通讯;1999年01期

2 李荆洪;;浅谈区域计算机联锁系统[J];郑铁科技通讯;2003年01期

3 郭掾龙;;全电子计算机联锁系统研究[J];科技经济导刊;2018年14期

4 李笑涵;殷田一男;杨扬;;车站计算机联锁系统配置信息软件设计[J];铁路计算机应用;2016年12期

5 陈建译;周荣;乔高锋;王海峰;徐田华;;基于故障数据的计算机联锁系统寿命预测方法[J];铁路计算机应用;2017年01期

6 陈光;;基于监测数据的计算机联锁系统安全性研究[J];铁道通信信号;2017年02期

7 李耀;张亚东;郭进;晏姗;饶畅;曹雅鑫;;铁路计算机联锁系统安全关键软件的安全性能建模方法[J];中国铁道科学;2017年02期

8 齐志华;彭阳;徐德龙;;计算机联锁系统操作显示界面优化设计[J];铁道通信信号;2017年07期

9 李红云;;拉萨至林芝铁路计算机联锁系统方案探讨[J];高速铁路技术;2017年05期

10 崔莉;;主流计算机联锁系统特点分析[J];无线互联科技;2016年12期

相关会议论文 前10条

1 宋钢;;关于移动式计算机联锁系统的研究[A];新世纪 新机遇 新挑战——知识创新和高新技术产业发展（上册）[C];2001年

2 芦树晴;;铁路计算机联锁软件智能测试系统[A];高速铁路与轨道交通（金融版）[C];2016年

3 段武;;城市轨道交通计算机联锁系统[A];中国城市轨道交通新技术（第三集）[C];2009年

4 潘明;何梅芳;张萍;赵阳;赵永青;;计算机联锁安全电子终端及其冗余组态的研究[A];铁道科学技术新进展——铁道科学研究院五十五周年论文集[C];2005年

5 陈福涛;张富春;;EI32-JD计算机联锁系统常见故障处理[A];河南省铁道学会2007年学术活动月优秀论文选集[C];2007年

6 刘聪芳;;浅谈JD-1 A型计算机联锁系统原理结构及故障处理[A];第十届中国科协年会中部地区物流产业体系建设论坛专辑[C];2008年

7 徐庆宁;;基于HJ04A的铁路信号计算机联锁系统[A];中国计量协会冶金分会2009年年会论文集[C];2009年

8 臧永立;;TYJL-Ⅲ型国产容错计算机联锁系统研究[A];铁道科学技术新进展——铁道科学研究院五十五周年论文集[C];2005年

9 张新明;王俊高;;二乘二取二冗余计算机联锁系统的结构与安全性分析[A];铁道科学技术新进展——铁道科学研究院五十五周年论文集[C];2005年

10 陈福涛;张富春;;EI32—JD计算机联锁系统常见故障处理[A];河南省铁道学会2007年学术活动月优秀论文集[C];2007年

相关重要报纸文章 前10条

1 王培莲　本报记者 白雪;谁在驾驭最先进的轨道交通[N];中国青年报;2011年

2 董萍;计算机联锁系统上列车运行更安全[N];中国教育报;2000年

3 山西省原平市卫生学校 王智丽;计算机联锁系统安全可靠性分析[N];山西科技报;2014年

4 通讯员 王冬　朱仁敏;卡斯柯产品通过高新技术成果转化认定[N];人民铁道;2009年

5 孙清华 李世伟;武广线信号改造工程首战告捷[N];山西日报;2000年

6 本报记者 矫阳;给高铁安上顺风耳[N];科技日报;2015年

7 杭庆博;黄矿铁运公司铁路数字化改革获得成功[N];延安日报;2011年

8 记者 唐骏W

本文编号：2665189