原创《形式化验证在轨道交通领域的应用》：本论文为您写形式化毕业论文范文和职称论文提供相关论文参考文献，可免费下载。
摘 要：随着轨道交通跨越式发展,越来越多的现代科技、国防和国民经济领域依赖轨道交通.轨道交通的安全性和可靠性成为国家和人民关注的重点.由于轨道交通領域的特殊性,传统的模拟和测试方法不能保证软件和硬件的可靠性.形式化方法可以保证从软件需求到软件编码全过程的逻辑一致性.最近几年,工程和学术界广泛使用形式化验证来对软件进行建模.该文介绍了形式化验证在轨道交通领域的应用,这包括软件需求、设计的形式化描述和软件的形式化建模.
关键词：轨道交通；形式化验证；形式化建模；形式化方法
中图分类号：TP301 文献标识码：A 文章编号：1009-3044（2018）13-0263-02
1 背景
随着一带一路战略性规划的稳步推进,轨道交通作为我国国民经济的命脉,其发展获得了令人瞩目的成绩.无论是硬件方面还是软件方面,轨道交通的安全性和可靠性一直是工程师关注的重点.由于对软件需求和设计的非形式化描述使软件开发缺乏统一的标准,使得轨道交通领域的研发受到限制.近年来,无论是在硬件设计还是软件系统方面,形式化验证（Formal Verification）取得了一批有规模的实用型研究成果,其中在轨道交通领域也取得了巨大的进展.该文介绍了在轨道交通领域如何使用形式化方法对系统进行建模和分析.
2 形式化验证的概念
形式化验证通过对系统进行穷尽搜索来进行验证,它以某个或某些形式的规范或属性为依据,使用数学的方法证明其正确性.形式化验证使用严格的数学推理来表明设计符合其全部或部分规范,这就要求使用形式化的描述来表达规范和实现.这些描述由符号框架给出,其形式语义明确地将数学对象与每个描述相关联,允许这些对象在正式的数学框架中被操纵.形式化验证可以分为三类：等价性验证（Equivalence Checking）、模型检验（Model Checking）和定理证明（Theorem Prover）.
等价性验证的基本思想是验证两个电路模型结构是否等价[1].主要用于验证门级与门级之间、RTL级与门级之间是否一致.在时钟树综合和扫描链重排等过程中,等价性检验可以确保门级网表的一致性.对于设计者手误导致的门级网表错误,等价性验证可以通过检测不一致来发现其中的错误.
模型检验用时态逻辑来描述规范,通过生成穷尽的且有效的搜索方法来检测系统是否满足给定的规范.主要是对系统或模型的运行状态创建一个有限自动机的抽象模型M,使用形式化语言对所要验证的性质创建描述规范说明.模型检验可以自动运行,不需要人工给出穷尽的测试用例来判断模型M是否能满足规范说明.模型检验能自动产生使命题不成立的反例,以解释命题不成立的原因[2].
定理证明把系统与规范都使用数学逻辑公式来表示,通过判断数学公理的正确性来寻求系统的描述.定理证明被用来表明实现的是规范的一个改进,这个实现在功能单元、寄存器级或门级被描述.
3 形式化建模
形式化验证使用严格的数学概念和语言,根据系统的需求来描述软件的定义和语义,从而对系统建模.从广义上讲,形式化建模是离散数学在软件工程上的应用,其涉及建模和分析,并具有数学上精确的符号.从狭义上讲,形式化建模是一系列具有明确定义的字符串,并且带有一套正式的规则来定义它的语法和语义.规则可以用来分析表达式,以确定它们是否在语法上良好地描述或证明它们的属性.目前有两种使用比较多的形式化建模语言,分别是Petri网和Pi验算.Petri网于20世纪60年代由Carl Adam Petri发明的.主要使用数学方式来描述离散并行系统,并且多用于对描述异步的、并发的系统进行建模.Pi演算是Robin Milner在20世纪80年代提出的,用于描述和分析并发系统,并用演算来描述进程之间的动态演化[3].
4 轨道交通领域的应用
近年来,作为国内外热门研究点,形式化验证发展迅速,相对于大规模测试,它从逻辑上验证了系统是否正确.形式化方法已成为确保软硬件设计质量和正确性的替代方法,克服了传统验证技术（如仿真和测试）的一些局限性.形式化方法在工程上的应用涉猎广泛,主要有两个方面：用于指定设计所需属性的正式框架,以及用于推导规范与相应实现之间关系的验证技术和工具.形式化验证已经被用于各种应用程序中,包括通信协议、硬件功能、软件功能和安全.这些应用表明,在一定条件下,形式化验证不受仿真指数增长率的影响,其机制保证了被证明的行为是通过物理设备的抽象模型来实现的.许多工程师使用形式化方法对汽车电子基础软件进行验证,以确保其安全性.
在轨道交通领域,形式化验证被更多地用于对系统的需求和设计进行形式化描述.文献[4]通过使用时间自动机网络模型对轨道交通运行控制系统进行形式化建模和验证,并使用时间自动机模型对系统的需求和设计进行精确描述,从而大大提高了轨道交通列车运行控制系统的安全性和可靠性设计水平.形式化建模可以辅助技术人员对系统描述进行建模.文献[5]使用进程代数方法对AUTOSAR存储保护机制建立形式化模型,从而实现一种操作系统的存储保护机制.文献[6]使用层次化有色Petri网,依据信号联锁逻辑的系统描述,对铁路车辆计算机联锁软件进行形式化建模.形式化验证可以给出系统的安全性和可靠性分析.文献[7]在高速铁路列控中心引入安全因子概念,采用安全行为模型,对不同类型的列控中心软件行为进行定义,从而实现对高铁列控中心的安全描述.文献[8]建立随机Petri网表示的CTCS无线通信机制模型,证明了Petri网可以辅助在移动闭塞区间对高速列车进行形式化建模和可靠性分析,并给出了故障定位信息的描述方法.形式化验证工具UPPAAL是用于实时验证系统的工具箱.它由两个主要部分组成：图形用户界面和模型检查器引擎.用户界面以Ja实现,并在用户工作站上执行.UPPAAL在工程界被广泛用于实现系统的仿真和分析.文献[9]利用时间自动机理论对车辆与地面交互流程进行建模,并使用形式化验证工具UPPAAL来模拟和分析对CTCS-3级列控系统.
5 结束语
形式化验证在轨道交通的各个层次都得到了应用,包括需求、设计、建模和分析阶段.相对于传统的模拟和测试方法,形式化验证不需要穷尽测试用例,更高效准确地保证了轨道交通系统的安全性和可靠性.
参考文献：
[1] 杨泽民, 范全润. 硬件设计的形式化验证技术[J]. 太原师范学院学报： 自然科学版, 2007, 6（2）： 54-56.
[2] 沈胜宇. 模型检验的反例解释[D]. 长沙： 国防科学技术大学, 2005.
[3] 周建儒. 软件形式化建模方法探析[J]. 河北软件职业技术学院学报, 2016, 18（2）： 48-50.
[4] 燕飞. 轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D]. 北京： 北京交通大学, 2006.
[5] 李青, 朱晓冉, 郭建. AUTOSAR OS存储保护机制的形式化验证框架[J]. 计算机工程, 2017, 43（1）： 79-85.
[6] 陈邦兴, 吴芳美. 铁路信号联锁逻辑形式化建模研究[J]. 铁道学报, 2002, 24（6）： 50-54.
[7] 喻钢, 刘晓文, 熊静, 等. 高速铁路列控中心软件安全性需求形式化建模[J]. 铁道学报, 2013, 35（7）： 74-79.
[8] 陈永, 王晓明, 党建武, 等. 基于SPN的CTCS无线通信形式化建模与分析[J]. 铁道学报, 2011, 33（8）： 63-68.
[9] 刘中田, 吕继东, 孙伟亮. CTCS-3级列控系统车地交互流程形式化建模与验证[J]. 北京交通大学学报, 2011, 35（2）： 76-81.
形式化论文参考资料：
结论：形式化验证在轨道交通领域的应用为关于形式化方面的论文题目、论文提纲、形式化论文开题报告、文献综述、参考文献的相关大学硕士和本科毕业论文。
