基于Event-B的联锁进路控制建模验证方法研究

童湖东，宁 滨，王海峰

（1.北京交通大学 轨道交通控制与安全国家重点实验室， 北京 100044；2. 北京交通大学 轨道交通运行控制系统国家工程研究中心， 北京 100044）

联锁系统是铁路信号系统的重要组成部分，是安全苛求系统。传统的联锁软件开发采用软件工程方法，采用自然语言定义需求，使用基于功能的方法进行系统设计，通过仿真和测试来进行系统的验证。此方法在系统需求描述上难以保证完整性和一致性，在功能上也很难进行完整的安全性分析与设计，仿真测试也无法完全遍历系统所有状态，使得联锁软件中的错误和安全隐患随应用的复杂度增加而增加，难以有效控制。针对这一问题，近年来国内外学者做了形式化方法运用于联锁软件定义、设计过程的研究，如使用命题逻辑[1]、形式化Z语言[2～3]来做联锁系统规格说明和安全需求定义，使用Petri网[4]等形式化工具对联锁设备和逻辑进行形式化建模等，但较少考虑对实际软件开发过程的支持，在应用上受到一定限制。

本文选取Event-B形式化方法对联锁进路控制过程相关功能需求和安全需求进行形式化建模、精化，采用机器证明和交互式证明相结合的方法进行验证，生成高可靠性的模型，为后续程序开发提供支撑。

1 Event-B简介

Event-B方法是一种基于模型的形式化建模验证方法，以集合论和一阶谓词逻辑作为数学基础，使用抽象机符号体系（Abstract Machine Notion， AMN），其构建系统模型的基本单元是描述系统静态属性的场景（context）和描述系统动态行为的抽象机（machine）。场景包含了系统中的常量（constant）、常量集合（carrier sets）以及用于约束常量（集合）类型、属性及相互关系的公理（axioms）和定理（theorems）；抽象机则包括了描述系统状态的变量（variables）、刻画状态改变的事件（event）及系统演变即状态变化过程中必须满足的不变式（invariants）。卫条件（guard）是事件发生的触发条件。Event-B以精化的形式进行模型的逐步扩展、细化和完善。为确保模型的安全性、有效性和完备性以及模型精化过程中的一致性，公理、定理和不变式需要被证明，由此产生证明义务[5]。Event-B相对于其他形式化方法更注重面向实际系统开发，从模型建立、精化、自动证明到代码生成整个开发周期都拥有较丰富的商业和开源的工具集支持体系。

2 联锁系统进路控制的Event-B模型

2.1 联锁静态数据的初步建模

联锁系统中静态数据的主要内容是信号机、道岔、轨道区段等物理实体的静态属性（如名称、位置）和构建于轨道区段之上的进路的静态属性（如性质、方向、范围）以及它们之间的制约关系。以图1所示站场图（部分）为例，1股道下行接车进路按方向依次包括轨道区段1DG、1G，Ⅱ股道下行接车进路则依次包括轨道区段1DG、ⅡG。

图1 站场示意图

Event-B中的笛卡尔积、关系、函数能很好地描述静态数据相关属性。在Event-B中，有如下定义：

定义1 笛卡尔积：对任意集合S、T，笛卡尔积S×T表示所有这样的有序对的集合：有序对中一个元素属于S,另一个元素属于T。即：S×T={a↦b|a∈S∧b∈T}。

定义2 关系：对任意集合S、T，关系S↔T表示S与T笛卡尔积的幂集，即：S↔T=ℙ(S×T)，是一个S到T的多对多映射，其中ℙ代表幂集。关系的定义域（dom）定义为：∀r·r∈S↔T⇒ dom(r)={x·(∃y·x↦y ∈ r)}；值域（ran）则定义为：∀r·r∈S↔T ⇒ ran(r)={y·(∃x·x↦y∈r)}。定义域限制定义为：S◁r={x↦y∣x↦y∈r∧x∈S}；定义域缩减 ：S◁r={x↦y∣x↦y∈r∧x∉S}。值域限制和缩减的定义类似。

定义3 函数：函数是一种特殊的关系，是一种多对一的映射。本文主要用到的Event-B函数定义如下，对任意集合S、T：

偏函数：S■T={r·r∈S↔T∧r～∘ r⊆T◁id}，其中r～是关系r的共轭关系，r～∘ r表示r～与r的复合；

全函数：S→T={f·f∈S■T∧dom(f)=S}；

偏内射：S■T={f·f∈S■T∧f～∈T■S}；

偏满射：S■T={f·f∈S■T∧ran(f)=T}。

在进路控制初步模型中，将轨道区段和进路以常量集的形式引入场景中，分别为集合BLOCK和ROUTE，以图1所示为例，BLOCK中的元素有 1DG， Ⅱ G，2DG和 1G；ROUTE则 包 含 了 1股道下行接车进路和Ⅱ股道下行接车进路。

为描述轨道区段间的拓扑连接关系以及轨道区段和进路之间的从属关系，引入以下常量：全关系adjc，描述轨道区段间的邻接关系；全满关系rbl，描述轨道区段与进路间的从属关系；全函数fbl和lbl，分别表示进路中第一个和最后一个轨道区段。轨道区段和进路的静态安全属性主要有以下几点：（1）进路内的轨道区段具有拓扑连续性。（2）不存在环形进路，即进路内的轨道区段不能首尾相接。（3）2条进路若有共用轨道区段，则共用部分必须是从第一区段开始或以最后一个区段结束的连续区段。初步模型中，静态安全属性用模型的场景部分的公理来描述。初步模型的场景结构如图2所示。其中am_nocircle、am_successive、am_nobreak1和am_nobreak2分别描述了上述的3条安全属性。

2.2 进路控制过程的初步建模

联锁软件进路控制过程总体上可划分为进路建立和进路解锁2个阶段[6]。本文用抽象机为进路控制过程建模，初步模型中主要考虑进路建立和进路解锁相关功能和安全需求的定义。在初步模型的抽象机interlocking_m_0中，引入4个模型变量表达系统状态：被选出的进路集合srt，被锁闭的进路集合lkrt，被征用的轨道区段集合sbl，以及被占用的轨道区段集合ocub。系统的安全需求分为2类：（1）状态固有属性的要求，即状态的归属和范围（用不变式1～5建模，如图3所示）；（2）系统演变中的状态迁移必须满足的规律，例如轨道区段状态只能是空闲→征用→锁闭→占用而不能反转（用不变式6～8建模，如图3所示）。对应于进路控制过程的功能需求，引入3个基本事件：进路选择route_select、进路锁闭route_lock和进路解锁route_unlock。相应的安全规则由事件的卫条件来描述，如进路锁闭的判断检查条件：（1）进路空闲；（2）相关道岔位置正确；（3）敌对进路未建立。对应图1站场图中，如要锁闭1股道上行接车进路，则必须要求1DG、1G空闲，道岔1处于反位锁闭状态。

图2 进路控制初步模型的场景结构

图3 进路选择、进路锁闭事件在初始模型抽象机中的结构

进路解锁与进路建立相对应，初步模型中考虑正常解锁，即在轨道电路检测条件下的自动解锁，且以3点检查方式作为安全性判断条件，即第一阶段检查是否前一区段已解锁和本区段有车占用，第二阶段检查本区段空闲和下一区段占用。

对应图1中，如要解锁1股道上行接车进路中的区段1G，则要求在紧邻的上一周期1DG处于解锁状态且1G占用，本周期1G空闲且2DG占用。3点检查解锁条件作为系统的安全需求以卫条件的形式引入事件的模型结构。进路解锁事件的模型结构如图4所示。

2.3 模型的精化

对于本文联锁系统的Event-B模型，精化的过程主要是将站场元素逐步完善、联锁功能需求和安全需求逐步纳入。本文采用了3步精化的策略，生成最终的进路控制模型，详细的精化策略如表1所示。

表1 进路控制Event-B模型的精化策略

图4 进路解锁事件的结构

在精化策略的框架下，通过对模型的场景加强、事件扩充和抽象机的细化分解，最终得到了较成熟的进路控制Event-B模型，整个模型的层次化继承结构如图5所示。

图5 进路控制Event-B模型的层次化继承结构

3 模型的形式化验证

Event-B采用基于定理证明的演绎验证的方式进行形式化验证，本文利用Rodin工具平台对设计的进路控制Event-B模型进行验证，Rodin能自动生成证明义务，并由自带的证明器独立自动证明部分证明义务。本文模型各精化层次的证明义务和自动证明数目见表2。

表2 各精化层次模型的证明义务数目和自动证明数目

对于未能被自动证明的证明义务，则通过Rodin提供的推导规则库机制、证明策略及相关工具，人为的增加一些假设条件和规则，进行人工引导下的交互式证明。

图6 证明义务route_select/inv8/INV的交互式证明过程

如图6所示，给出了抽象机rtcontrol_m_0中证明义务route_select/inv8/INV的交互式证明主要过程，该证明义务描述了事件route_select是否满足不变式inv_8。自动证明器通过引入自由变量r0进行证明，实际上要证明相继式1。该过程中需要手动加入待证明的假设(rbl▷{r})～[{r0}]=∅，证明器利用已有假设对该假设做出证明后，整个证明义务的推导证明就会由证明器继续往前推进。

经过上述步骤，对整个模型的证明义务进行了完全的证明，模型的安全性和正确性得到保证，为后续利用Event-B模型到代码转化相关工具生成高可靠性的进路控制程序打下了基础。

4 结束语

联锁系统具有逻辑上的复杂性和安全苛求特性，本文针对传统开发方法存在的需求定义不精确，软件安全隐患不易排除等缺点，探索了利用Event-B形式化方法对联锁软件的核心部分—进路控制过程进行建模和验证的方法：利用形式化Event-B语言严格描述系统安全需求和功能需求，通过逐步精化来构建系统模型，并通过基于定理证明的验证方式进行模型验证以保证模型的安全性和一致性。结果表明，Event-B方法能较好运用于联锁软件开发过程，弥补传统开发方法的不足。

[1]Eugenio Roanes-Lozano, Antonio Hernando, Jose Antonio Alonso, Luis M. Laita. A logic approach to decision taking in a railway interlocking system using Maple[J]. Mathematics and Computers in Simulation, Volume 82, Issue 1, September 2011, Pages 15-28.

[2]Khan, S.A.; Zafar, N.A.Towards the formalization of railway interlocking system using Z-notations[C]. 2nd In-ternational Conference on Computer, Control and Communication, vol.,no., pp.1-6, 17-18 Feb. 2009.

[3]王铁江，郦 萌. 计算机联锁软件的Z规格说明[J]. 铁道学报，2003，25（4）：62-66.

[4]陈邦兴，吴芳美. 铁路信号联锁逻辑形式化建模研究[J].铁道学报，2002，24（6）：50-54.

[5]Jean-Raymond Abrial. Modeling in Event-B[C]. Cambridge University Press，2010.

[6]赵志熙. 车站计算机联锁ABC[M]. 北京：中国铁道出版社，2007.