基于Petri网的列控系统形式化分析方法

0引言

软件开发方法有结构化开发方法、面向对象开发方法和形式化开发方法等。结构化开发方法和面向对象开发方法在分析和设计过程中，系统规格说明可能包含二义性、含糊性、不完整性及抽象层次混杂等问题，这将很难保证软件的开发质量。对于安全性要求很高的大型系统，任何微小的软件错误都可能导致生命危险和严重的经济后果，因此形式化开发方法在大型软件的开发过程中得到了越来越多的重视。

形式化软件开发方法是建立在严格数学基础上，具有精确数学语义的开发方法。它分为形式化规格说明和形式化验证。形式化规格说明是通过具有明确数学定义的文法和语义方法或语言对软件的期望特性或行为进行精确、简洁的描述；形式化验证是基于已建立的形式化规格说明对软件的相关特性进行评价的数学分析和证明。形式化开发方法可以帮助软件工程师创建更为简洁、准确、无歧义的规格说明，进而通过严格的验证分析发现设计及开发过程中的不一致性、模糊性和不完备性，以达到对软件质量、开发成本及开发进度的有效控制。

目前，大型软件开发技术的完全形式化还只停留在理论研究层面上，但是国内外从事于相关领域的相关人员已经做出了相当深度的研究，并且开发出一些系统的软件开发平台，在应用层面上形式化开发技术和仿真技术相结合是目前大型软件开发技术发展的一种潮流[1]。

Petri网是目前较好的一种形式化软件开发技术。它可以很好地描述具有并发、异步、不确定性的信息处理系统。目前Petri网已经在自动控制、操作系统、并行编译、网络协议、离散事件动态系统、混杂系统、柔性制造等许多科学技术领域得到了广泛应用。

列车控制系统是保障运营效率和安全的重要手段，它将先进的控制技术、通信技术、计算机技术与铁路信号技术有机地联系在一起，充分保障了现代铁路行车安全并提高了运行效率。但列车控制系统组成单元多，物理系统复杂，需要各个子系统协同配合工作才能保证系统的正确运行，属于大规模的、实时性和可靠性要求高的控制系统。作为列车群运行控制的核心，列车群行为建模问题一直都没有得到很好的解决。文献[2-5]仅对列车的进出站的调度给出了Petri网的模型，并未对列车的区间运行控制进行讨论，其模型的验证用的是仿真方法。Petri网本身是一种很好的形式化工具，有着丰富的验证工具如不变量、进程、同步性、结构性等。文献[2-5]缺乏形式化验证的内容，是一个非常大的遗憾。

本文将带有抑止弧的增广Petri网引入到列车控制系统的一些关键技术的建模中来，构建了一类具有自动控制功能的列车运行控制系统。系统较全面地模拟了列车运行控制的整个过程，区间运行阶段对铁路公路交叉系统进行了建模，确保了人员密集区域的行车安全，并重点对雷击等意外事故的发生建立了应急处理系统，确保了行车安全。最后对模型进行了正确性的分析。

有关原型Petri网的概念见文献[6-9]，有关列车控制的基本概念见文献[10]。