形式化方法应用于计算机联锁软件的安全验证研究

罗 娟，王燕芩

（卡斯柯信号有限公司，上海 200071）

形式化方法应用于计算机联锁软件的安全验证研究

罗 娟，王燕芩

（卡斯柯信号有限公司，上海 200071）

铁路信号系统中的联锁系统对安全性要求极高，仅通过普通的功能测试无法保障其安全性。采用形式化验证的方式可以验证联锁系统的应用逻辑与安全需求的一致性。将通用安全需求结合具体的站场图进行实例化，得到具体的安全需求后输入带归纳功能的布尔可满足问题（SAT）约束求解器进行验证，通过覆盖所有的实例、所有周期以及每个周期所有的状态空间，保证了验证方法的完备性。

计算机联锁；安全需求；通用应用；形式化验证

联锁系统是涉及到生命财产安全的高安全性系统，其安全性除了体现在冗余结构的系统硬件上，还应考虑系统软件的安全性。软件的安全性需通过系统逻辑设计与安全需求的一致性和特殊的安全防护措施保证。在安全需求实现时，若存在系统需求描述不准确，则会造成需求设计实现不准确，这一系列因为人为失误可能导致最终的系统功能失效，威胁行车安全。为了确保系统需求的正确实现，本文提出形式化方法对既有联锁系统应用进行安全验证，确保系统实现与安全需求要求的一致性。联锁系统是铁路信号系统中的安全相关的重要系统，根据EN50128的要求，联锁系统的安全性需达到SIL4的安全等级，因此对其进行安全验证十分必要。

1 研究背景

对于安全相关的系统，在正常功能性需求外，含大量安全需求。其中，功能需求描述了系统正常的功能总会在未来某个正确的时刻发生，而安全需求则描述了导致系统危险的情况不会发生[1]。传统的开发、设计和测试的方法不能保证系统所有安全需求均被正确实现。目前，系统的功能需求主要通过测试的方法进行验证，而安全需求则主要通过危险分析（HA，Hazard Analysis）及创建危害日志的方法，分析和记录系统可能出现的危险。采用传统的开发、测试和验证主要存在以下几个方面的缺点：

（1）使用自然语言描述需求，需求内容不够明确，容易产生二义性，设计和测试阶段均可能会出现因为对需求理解的偏差而造成设计错误或测试错误的情况；

（2）传统的测试采用人工设计测试用例的方式，对于某一个功能的所有场景可能无法考虑全面，从而导致测试用例设计不完整；

（3）传统的测试过程无法覆盖系统在某个测试场景下所有的状态空间，导致系统运行过程中发生的危害并不能通过测试发现；

（4）对于安全需求的验证目前主要是通过追踪需求、设计、实现中的对应关系进行，大多仅停留在文档的层面，无法保证软件的实现完全满足安全需求。而且多采用人工分析的方式，效率较低，需要投入较多的人力资源。

2 形式化方法简介

2.1 形式化方法

形式化方法[2]是建立在严格数学基础上、具有精确数学语义的开发方法，能够除去用自然语言描述而造成的需求、属性方面的模糊定义。该方法需要对被验证对象进行形式化建模，也就是将一般的需求定义抽象成数学模型，将待测系统抽象成可被证明的数学模型。

形式化方法可分为形式化规范描述和形式化验证两大类：（1）形式化规范描述使用具有严格数学定义的语法和语义的规范语言来描述系统。被描述的系统特性包括行为特性、时间特性、性能特性和内部结构等。采用形式化语言将非形式化的（Informal）需求进行形式化（Formal）描述，从系统设计的开始阶段就努力降低系统的故障率，可以节省大量后期调试、修改成本。（2）形式化验证是通过数学证明的方式，自动化的验证系统在一定的前提条件下满足各种静态和动态性质。

2.2 形式化验证主要技术

形式化验证的主要技术包括模型检验和定理证明：（1）模型检验是一种基于有限状态模型并检验该模型的期望特性的技术。它对模型的状态空间进行遍历搜索，以确认该系统模型是否具有某些性质。（2）定理证明则是选定一个数学逻辑体系，用体系中的公式描述系统和系统性质。依据该体系中的公理和定理，推导系统性质的描述公式。

定理证明因其在验证过程中需要人工交互而导致自动化程度不高，相比于定理证明，以模型检验的方法则可以对系统变量进行全状态空间的检验和证明，在提升系统状态覆盖完备性同时，提高了验证的自动化程度。

法国巴黎地铁14号线的自动驾驶系统就是用形式化方法开发并验证的，1998年投入运行，至今未发现任何缺陷。法国戴高乐机场用于接送乘客无人驾驶线路也应用形式化方法对系统安全性进行了验证。

3 联锁系统软件的形式化验证

随着铁路信号控制系统的复杂性在不断地增加，世界各大业主和信号厂商也越来越重视形式化方法的应用：（1）形式化验证方法从系统的安全需求出发，通过模型检验，证明系统的安全需求已经实现且系统功能满足安全需求的要求，验证系统安全性确实满足既定要求；（2）通过验证，检验系统在安全实现上的缺陷，做到查漏补缺，能够早发现，早解决，为系统的安全提供安全保障；（3）形式化验证在系统的全状态空间的搜索过程中，能够完整检验系统在任意状态可能潜在的风险问题，增强产品信心。

将安全需求的形式化验证方法应用于联锁系统，需要考虑在实际控制应用过程中的特殊性。联锁系统软件内部逻辑主要是布尔逻辑，从状态空间的角度出发，对其进行模型检验更为可行。对于联锁系统而言，危及行车安全的风险主要有列车或车列迎面冲撞、侧面冲撞、追尾冲撞、错道、挤岔和掉道等。对于一个完善的联锁系统，除了要通过测试说明各项功能需求被正确无误的实现，还必须要验证导致上述各种危险的事件不可能发生。采用归纳验证和模型检验相结合的形式化验证方法用于确保系统的输出确实无法导致危险事件发生。其中，通过模型检验可以覆盖每一个周期的所有状态空间，而通过归纳验证，则可以覆盖所有的周期。

3.1 验证流程

本文所描述的是通过开发通用的形式化安全需求，结合具体站型对实例化后的既有联锁应用进行形式化验证的过程。其中，所涉及到的联锁系统逻辑的通用应用和特定应用都是以布尔表达式进行描述。对联锁系统特定应用进行形式化验证的过程如图1所示，主要包括：（1）联锁系统安全需求通用建模及针对特定应用的配置，即图中两个虚线框内的部分。这两部分完成后，就可以直接输入到实例化工具中，将通用安全性质实例化为针对特定站场的特定安全性质；（2）将特定安全性质输入到带有归纳证明功能的模型检验的验证器中进行形式化验证，得到最终的结果，并通过对最终结果的分析确定系统是否满足相关的安全性质。其中，针对安全需求通用建模，主要是建立联锁信号设备的逻辑模型，用以描述联锁功能上的逻辑关系，同时，设计形式化安全需求与应用的接口，以实现后续安全需求实例化。

图1 联锁软件形式化验证流程

3.2 安全需求形式化描述

为了能够实现安全需求的形式化验证，要求验证输入的需求必须以形式化方式进行描述。用于安全需求形式化描述的语言很多，本文提出了一种基于面向对象技术和一阶谓词逻辑[3]的形式化语言。

面向对象的技术可以很好地对验证系统的各功能模块及控制对象进行建模，而一阶谓词逻辑能够清楚地描述各个控制对象之间的联锁关系，且能够通过实例化和变换转变为析取范式，便于验证器进行验证。该语言由基本的逻辑操作符（如and,or,not,=＞）、量词（如ALL,EXIT）组成，具有面向对象的继承、方法重载等特性。基本的操作元素是对象，每个对象属于一个类，类包括属性、函数、等式等字段。例如，对于安全需求“进路开放，则进路上的区段空闲”而言，对该条安全需求采用形式化方式描述后即为：

"ALL rt(rt.route_clear =＞ ALL seg(rt.segment(seg) =＞seg.vacant))",(PO1)

其中，rt,seg分别为事先定义的控制对象的应用实例，route_clear,segment，vacant是控制对象需实现的功能函数。

3.3 安全需求实例化

本文所述的联锁系统形式化验证的应用是对具体的联锁应用逻辑进行形式化验证，而上述形式化安全需求是从通用角度进行描述的，因此，为了能够进行最终的验证工作，还需要对安全需求进行实例化。从通用的安全需求转换为针对具体某个站的安全需求的过程称为安全需求实例化。安全需求实例化实际就是将每条形式化安全需求中的对象实例化为站场上对应的设备，而功能函数则通过函数描述的关系最终转换为每个设备对应的参数。从数学层面来看，整个实例化的过程就是在类实例化和函数映射的基础上移除全称量词和存在量词的过程。由于这一过程完全可以通过面向对象技术结合相应的数学原理实现，因此这一过程可以由工具自动完成。

3.4 安全需求与通用应用接口

由于是对既有联锁应用进行形式化验证，而联锁系统逻辑并非用上文提出的形式化语言进行设计和描述，因此，从形式化语言到联锁通用应用逻辑之间必须建立映射关系，以支持安全需求的实例化。

安全需求与通用应用接口主要包括以下工作：站场信号设备面向对象建模、站场平面图信息读取、信号设备模型与站场图和通用应用的映射。

3.4.1 站场信号设备面向对象建模

结合联锁系统功能，在建模时，通用设备对象的分类采用面向对象的方式，因此，需要对信号设备分类，主要包括：进路、信号机、道岔、轨道区段，上述这些设备均可作为父类。如进路又包括列车进路、调车进路、非进路等。信号机根据不同的作用可分为：列车信号机、调车信号机和列车兼调车信号机。列车信号机主要是用来作为列车进路的始端或终端，调车信号机可以作为调车进路的始端和终端，而列车兼调车信号机，既可以作为列车进路的始终端，又可作为调车进路的始终端，但同一时间只能作为一种进路的始端或终端。上述给出的是基本的信号设备分类，考虑复杂的情况时还可以进一步扩展。对于每一个类，需要设计相应的参数、函数和等式。参数是可以直接从站场图中获得的信息，如信号设备之间的位置关系等；函数是信号设备的状态或功能描述，如信号机的开放或关闭状态；等式与函数很类似，但是与周期相关，即等式左边计算得到的值都是下一周期的值，需要使用本周期的值进行计算。另外，由于进路是由信号机、道岔和轨道电路组成，因此，还需要设计进路和其他3种设备之间的关系。图2所示为信号设备的面向对象的关系图。

图2 信号设备面向对象建模示意图

3.4.2 站场平面图信息读取

站场平面图信息的读取是为了提取出信号设备的属性以及各信号设备之间的拓扑关系，并将相关的信息传给对象结构中的函数和参数。站场平面图的描述一般采用结构化的文件进行，内部包括各种数据结构。本文描述的是以XML格式的站场图的信息提取。XML中包含的信号设备相关的字段主要有：SIGNAL,TRACK,SWITCH,ROUTE等，当然还包括一些零散的按钮和表示灯，在此就不进行介绍。表1以道岔为例，给出了其在站场描述文件中对应的各种字段。

表1 道岔属性表

3.4.3 信号设备模型与站场图和通用应用的映射

为了对信号设备以及安全需求进行实例化，需要建立信号设备模型到站场图和通用应用之间的映射关系，这里的映射关系包括两层：（1）信号设备模型到站场图的映射，进行该映射可以将站场图上的具体的信号设备与信号设备类联系起来，得到信号设备实例以及每个实例对应的拓扑关系相关的参数值。以信号机为例，根据type确定信号机父类，根据subtype确定子类，这样就可以产生一个信号机实例，再根据其他字段，可得到实例中相关参数的取值。（2）信号设备类中的函数、变量到通用应用逻辑中实际变量之间的映射，如对于轨道区段， TRACK类会有一个vacant的函数，用来表示区段的占用或空闲状态，那么在通用应用逻辑中会有一个相同含义的变量，如：用布尔变量DGJ表示区段占用（DGJ=0）或空闲（DGJ=1）。表2列出了一些主要的函数映射关系。

表2 主要信号设备类函数与联锁应用逻辑变量映射表

4 形式化验证实现

在联锁系统中，信号开放必须检查其内方轨道区段处于空闲状态[4]。由此出发，建立验证该安全需求的通用应用，即：若进路始端信号开放，则进路内方所有区段应空闲。在描述安全需求的通用验证模型外，必须结合特定的站型对通用模型进行实例化，以检验建立的通用模型满足安全需求，达到对安全需求验证的目的。

对上述安全需求进行形式化描述后得到：

"ALL rt(rt.route_clear=＞ ALL seg(rt.segment(seg) =＞seg.vacant))"，

其中，rt表示进路变量，seg表示区段，rt.segment(seg)表示区段seg是进路rt的内方区段，seg.vacant表示区段seg处于空闲状态，route_clear表示进路进路始端信号开放，但由于一个信号可能会是多条进路的始端信号，因此，将需求细化为“进路内方道岔位置正确，始端信号开放，则进路内方区段空闲”，将route_clear进一步定义为：

"route_clear (ROUTE rt) :=

EXISTsi(rt.start_signal(si) and si.permissive and ALL sw(rt.switches(sw) =＞sw.in_required_pos(rt)))"

其中，si表示信号机，rt.start_signal(si)表示信号机si是进路rt的起始信号机，si.permissive表示信号机si为允许状态，sw表示道岔，rt.switches(sw)表示道岔sw是进路rt内方的道岔，sw.in_required_ pos(rt)表示道岔sw当前所处的位置和进路rt要求的位置一致。

如图3所示：（1）进站信号机X的防护进路有3条，X-S1，X-SII，X-S3，对应的进路就会被实例化为上述3条；（2）根据站场图中的拓扑关系去实例化这3条进路的起始信号机、内方的道岔和区段；（3）当无论当前建立的进路是这3条进路中的哪一条时，验证结果均满足安全需求，才能够得到对于X信号机而言，满足“信号开放，进路内区段空闲”的安全性质。

图3 简单站场图示例

根据上述的站场图以及相关的映射关系进行实例化后共可以得到24条具体的安全需求并且全部通过验证。

实例化后进行安全验证主要是使用了带有归纳功能的布尔可满足问题（SAT）约束求解器进行模型检验。其中，SAT约束求解器的基本原理可以参见[5～8]。而归纳功能是针对联锁系统不同的周期而言的，SAT约束求解器只能针对一个周期进行求解，如果要求在任何周期都满足，那么就需要结合归纳法：（1）检查在初始周期是否满足相关的性质；（2）假设某一个周期K，系统满足相关的性质，进而去证明K+1个周期时，相关的性质也能够得到满足，那么就可以得到系统在任何时候都满足对应的性质。

5 结束语

联锁系统是安全相关的系统，其安全性仅仅通过测试无法保障，通过形式化验证的方式，可以遍历环境模型约束下每条安全需求每个周期的所有状态空间，而由于联锁系统软件逻辑结构比较简单，状态空间大小适中，对验证器的要求并不高，因此可以很好地进行形式化验证。本文所应用的方法可以在不开发形式化的通用应用模型的前提下，进行安全需求的验证，只需要开发通用应用模型与安全需求之间的接口即可，适用于对既有的联锁应用进行验证，可以作为联锁应用开发过程中的安全补强，增加对特定联锁应用安全性的信心。而且不需要从需求阶段就建立形式化模型，应用难度远小于一般的形式化方法。从验证的结果可以看到，通过对安全需求建模，对其进行实例化，再使用带归纳法的SAT约束求解器对实例化后的安全需求进行验证，可以很好地发现应用逻辑中不满足安全需求的地方，从而实现安全验证的目的。本文中所介绍的方法已经在相关实验项目中应用，使用真实的站型验证了其可行性。

[1]Nicolas Halbwachs,FabienneLagnier,Christophe Ratel.Programming and Verifying Real-TimeSystems by Means of the SynchronousData-Flow Language LUSTR[J].IEEE Transactions of Software Engineering,1992,18(9):785-793.

[2]古天龙.软件开发的形式化方法[M].北京：高等教育出版社，2005：15-22.

[3]石纯一，王家廞.数理逻辑与集合论[M].北京：清华大学出版社，2000：54-111.

[4]何文卿.6502电气集中电路[M].北京：中国铁道出版社，2007：112-132.

[5]童湖东，宁 滨，王海峰.基于Event-B的联锁进路控制建模验证方法研究[J].铁路计算机应用，2013，22（6）：57-61.

[6]季晓慧，张 健.约束问题求解[J].自动化学报，2007，33（2）：125-131.

[7]Y Vizel，G Weissenbacher，S Malik.Boolean Satisfiability Solvers and Their Applications in Model Checking[J].Proceedings of the IEEE,2015 (11):1-15.

[8]J Marques-Silva.Model checking with Boolean Satisfability[J].Journal of Algorithms,2008,63(1-3):3-16.

责任编辑 王 浩

Formal method applied to safety verifcation for computer interlocking software

LUO Juan,WANG Yanqin
( CASCO Signal Ltd., Shanghai 200071,China)

The Interlocking System is a safety critical system.Its safety cannot be guaranteed only by testing.Formal verifcation can be used to verify the consistency between the applied logic and the safety requirements of the System.In this article,the general safety requirements were instantiated with the specifc station layout.Then the specifc safety requirements were verifed through inputting them to the SAT induction constraint solver.The completeness of the method was guaranteed by covering all the instances,all the cycles and all the state space of each cycle.

computer based interlocking;safety requirement;general application;formal verifcation

U284.3∶TP39

A

1005-8451（2016）11-0053-05

2016-06-06

罗 娟，助理工程师；王燕芩，工程师。