论文部分内容阅读
摘要：随着现场总线技术、计算机网络通信技术、嵌入式系统控制技术以及故障诊断技术的高速发展，当前列车控制系统已经实现了从孤立的数字控制系统向基于网络的分布式控制系统的转变。在现下我国高速铁路迅猛发展的浪潮下，列车通信网络系统的自主研发、设备制造以及维护运营等课题引起了各大高校和研究机构的高度重视。然而，在列车客运业硕果累累的同时，其诸多问题在系统设计过程中变得日渐凸显。本文对基于形式化方法和模拟方法的列车系统建模及验证的相关研究进行了重点探讨。
关键词：列车通信网络；形式化建模；静态属性分析；形式化验证；模拟验证
我国幅员辽阔、人员众多的基本国情决定了构建安全可靠、经济环保以及实用快捷的高速列车的重要意义。随着二十一世纪初叶我国第一条高速铁路京津城际高铁的正式通车运营，我国从此迈入了高速列车时代。根据《中国铁路中长期规划》，二零二零年我国将建设二百公里时速以上的高速铁路长达约两万公里，以便满足人民群众日益增长的出行需要。随着列车通信网络的逐渐发展和创新升级，其取得了不菲的成就，然而在自主研发、设备制造以及维护运营等相关问题上尚未有切实可行的方案。但是我国铁路尚还处于起步阶段，迫切需要高速列车关键技术的技术支持。
一、列车通信网络系统的形式化建模概述
（一）UML
UML是Unified Modeling Language的英文缩写，又称为统一建模语言。UML是二十世纪末期由对象管理组织发布的一种建模语言，其具备定义良好、功能强大以及使用便捷等诸多优点，因而在业界得到了广泛使用[1]。UML支持对软件密集系统的可视化建模，并且具有面向对象语言的特征，即其理念是“让语言适应问题，而不是要问题适应语言”，它能够让开发人员关注与系统的模型和结构，而不是系统实现的具体细节，适用于数据建模、业务建模、对象建模以及组件建模等。
（二）Petri网
Petri网是德国科学家Carl Adam Petri博士于二十世纪中叶在其博士论文《Kommunikationmit Automaten》中首次提出的，然后经过了长达40余年的发展和完善，逐步形成的一種完整、系统的通用建模语言[2]。Petri网不仅可以勾勒系统的结构，还能描述系统的动态行为，当前其在计算机科学与技术、自动化科学技术、机械设计与制造、工业过程控制以及经济学等领域都得到了普及应用。Petri网是一种基于图形的数学建模语言，其既可以通过图形界面模拟系统的行为特征，又能够结合线性代数、矩阵论等相关数学理论对系统的性质进行有效的分析，Petri网的分类如图1所示。
Petri網理论经过业界多年的实践与完善，目前已经形成多层次、多分支的理论结构，从其外延上可以分为基本Petri网、有色Petri网、增广Petri网以及含时间因素的Petri网等，其中有色Petri网、增广Petri网以及含时间因素的Petri网均可以称作高级Petri网。高级Petri网是对基本Petri网的扩展和抽象，其能够做到对网中的托肯进行分类、解析和运算，减少网系统中国的基本元素，以便实现缩小网系统规模的目标[3]。高级Petri网的主要优势是当其对复杂的系统进行建模时，所建立的模型将更为简单、清晰以及直观。
（三）时间自动机
时间自动机是一种用于实时系统建模和验证的理论，其以基本有限自动机的为基础，并加入了实时变量建模时钟集合，时钟变量的限制用于控制自动机的行为，相关研究机构在其理论技术上开发了时间自动机属性验证工具，比如UPPAAL以及Kronos等，实现了自动化验证过程的高效执行。
二、列车通信网络系统的形式化验证方法
形式化验证过程如图2所示，较其他验证方法，其具备四大优势：第一，验证情况蕴含所有的激励空间，验证过程和理论是完整的；第二，验证结果的正确性以数学理论为保障，与系统的激励情况无关；第三，验证结果不需要建立参考模型，生成期望的输出序列；第四，当验证发现错误时，可以生成简单易懂的错误调试信息[4]。当前，形式化验证方法主要包括定理证明、模型检查以及等价性检查。
（一）定理证明
定理证明（Theorem Proving）的目标是借助公理和推理规则等形式化逻辑证明设计的正确性。在理论证明系统中，通过逻辑架构对设计进行描述，并用引理对一系列性质进行描述，引理需要通过一些推理规则证明正确性。一级逻辑和高级逻辑能够准确无误地实现系统信息的表达，进而有效规避了自然语言描述系统带来的不准确的风险。
定理证明系统可以处理复杂的逻辑运算，定理证明过程以公理、推理规则、中间引理以及派生定义为依托，一般而言，往往需要具有专业素养过硬的人员进行推理路线的选定，进而交互式的完成证明过程。
（二）模型检查
上世纪末期E.M.Clarke等提出了基于师太逻辑和有限状态转移图的模型检查方法之后，模型检查方法因为较定理证明方法具有更高的自动化程度的优势，而在世界上各个研究机构和实验室得到深入研究和普及应用，以后经过了许多年的实践和完善。模型检查方法以时态逻辑为基本思想，描述程序或电路的时序性质，使用Kripke结构表示程序或电路的行为和结构，通过Kripke结构验证其是否满足时态逻辑公式。
结语
综上所述，我国幅员辽阔、人员众多的基本国情决定了构建安全可靠、经济环保以及实用快捷的高速列车的重要意义。尽管高速列车网络系统仍存在一些问题，但是随着高速列车网络系统形式化建模和验证方法的实践和不断完善，我国的高速列车客运业到一定可以实现更为良好的发展。
参考文献：
[1] 孙立宏，洪一.？？基于VMM统一验证平台的处理器芯片功能验证[J]. 火控雷达技术. 2010（01）
[2] 陈江，陈建国，陆慧娟，王康健.？？UML时间顺序图的实时系统建模及验证[J]. 中国计量学院学报. 2010（01）
[3] 傅游，花嵘，田银花.？？基于带抑制弧的Petri网的min-min算法模型研究[J]. 计算机应用研究. 2010（01）
朱小艳，1985年10月28日出生，性别女，民族汉，籍贯安徽池州，单位中车南京浦镇车辆有限公司，邮编210032，职称助理工程师，学历硕士，研究方向列车通信网络
关键词：列车通信网络；形式化建模；静态属性分析；形式化验证；模拟验证
我国幅员辽阔、人员众多的基本国情决定了构建安全可靠、经济环保以及实用快捷的高速列车的重要意义。随着二十一世纪初叶我国第一条高速铁路京津城际高铁的正式通车运营，我国从此迈入了高速列车时代。根据《中国铁路中长期规划》，二零二零年我国将建设二百公里时速以上的高速铁路长达约两万公里，以便满足人民群众日益增长的出行需要。随着列车通信网络的逐渐发展和创新升级，其取得了不菲的成就，然而在自主研发、设备制造以及维护运营等相关问题上尚未有切实可行的方案。但是我国铁路尚还处于起步阶段，迫切需要高速列车关键技术的技术支持。
一、列车通信网络系统的形式化建模概述
（一）UML
UML是Unified Modeling Language的英文缩写，又称为统一建模语言。UML是二十世纪末期由对象管理组织发布的一种建模语言，其具备定义良好、功能强大以及使用便捷等诸多优点，因而在业界得到了广泛使用[1]。UML支持对软件密集系统的可视化建模，并且具有面向对象语言的特征，即其理念是“让语言适应问题，而不是要问题适应语言”，它能够让开发人员关注与系统的模型和结构，而不是系统实现的具体细节，适用于数据建模、业务建模、对象建模以及组件建模等。
（二）Petri网
Petri网是德国科学家Carl Adam Petri博士于二十世纪中叶在其博士论文《Kommunikationmit Automaten》中首次提出的，然后经过了长达40余年的发展和完善，逐步形成的一種完整、系统的通用建模语言[2]。Petri网不仅可以勾勒系统的结构，还能描述系统的动态行为，当前其在计算机科学与技术、自动化科学技术、机械设计与制造、工业过程控制以及经济学等领域都得到了普及应用。Petri网是一种基于图形的数学建模语言，其既可以通过图形界面模拟系统的行为特征，又能够结合线性代数、矩阵论等相关数学理论对系统的性质进行有效的分析，Petri网的分类如图1所示。
Petri網理论经过业界多年的实践与完善，目前已经形成多层次、多分支的理论结构，从其外延上可以分为基本Petri网、有色Petri网、增广Petri网以及含时间因素的Petri网等，其中有色Petri网、增广Petri网以及含时间因素的Petri网均可以称作高级Petri网。高级Petri网是对基本Petri网的扩展和抽象，其能够做到对网中的托肯进行分类、解析和运算，减少网系统中国的基本元素，以便实现缩小网系统规模的目标[3]。高级Petri网的主要优势是当其对复杂的系统进行建模时，所建立的模型将更为简单、清晰以及直观。
（三）时间自动机
时间自动机是一种用于实时系统建模和验证的理论，其以基本有限自动机的为基础，并加入了实时变量建模时钟集合，时钟变量的限制用于控制自动机的行为，相关研究机构在其理论技术上开发了时间自动机属性验证工具，比如UPPAAL以及Kronos等，实现了自动化验证过程的高效执行。
二、列车通信网络系统的形式化验证方法
形式化验证过程如图2所示，较其他验证方法，其具备四大优势：第一，验证情况蕴含所有的激励空间，验证过程和理论是完整的；第二，验证结果的正确性以数学理论为保障，与系统的激励情况无关；第三，验证结果不需要建立参考模型，生成期望的输出序列；第四，当验证发现错误时，可以生成简单易懂的错误调试信息[4]。当前，形式化验证方法主要包括定理证明、模型检查以及等价性检查。
（一）定理证明
定理证明（Theorem Proving）的目标是借助公理和推理规则等形式化逻辑证明设计的正确性。在理论证明系统中，通过逻辑架构对设计进行描述，并用引理对一系列性质进行描述，引理需要通过一些推理规则证明正确性。一级逻辑和高级逻辑能够准确无误地实现系统信息的表达，进而有效规避了自然语言描述系统带来的不准确的风险。
定理证明系统可以处理复杂的逻辑运算，定理证明过程以公理、推理规则、中间引理以及派生定义为依托，一般而言，往往需要具有专业素养过硬的人员进行推理路线的选定，进而交互式的完成证明过程。
（二）模型检查
上世纪末期E.M.Clarke等提出了基于师太逻辑和有限状态转移图的模型检查方法之后，模型检查方法因为较定理证明方法具有更高的自动化程度的优势，而在世界上各个研究机构和实验室得到深入研究和普及应用，以后经过了许多年的实践和完善。模型检查方法以时态逻辑为基本思想，描述程序或电路的时序性质，使用Kripke结构表示程序或电路的行为和结构，通过Kripke结构验证其是否满足时态逻辑公式。
结语
综上所述，我国幅员辽阔、人员众多的基本国情决定了构建安全可靠、经济环保以及实用快捷的高速列车的重要意义。尽管高速列车网络系统仍存在一些问题，但是随着高速列车网络系统形式化建模和验证方法的实践和不断完善，我国的高速列车客运业到一定可以实现更为良好的发展。
参考文献：
[1] 孙立宏，洪一.？？基于VMM统一验证平台的处理器芯片功能验证[J]. 火控雷达技术. 2010（01）
[2] 陈江，陈建国，陆慧娟，王康健.？？UML时间顺序图的实时系统建模及验证[J]. 中国计量学院学报. 2010（01）
[3] 傅游，花嵘，田银花.？？基于带抑制弧的Petri网的min-min算法模型研究[J]. 计算机应用研究. 2010（01）
朱小艳，1985年10月28日出生，性别女，民族汉，籍贯安徽池州，单位中车南京浦镇车辆有限公司，邮编210032，职称助理工程师，学历硕士，研究方向列车通信网络