基于标签转移系统的二乘二取二系统的形式化验证研究

付 伟

(中国铁道科学研究院通信信号研究所,北京 100081)

1 概述

随着铁路列车控制技术的快速发展，具有我国自主产权的CTCS列车控制系统在我国高速铁路上得到了广泛应用，有效保障了高速列车的安全运行[1]。CTCS系统中的计算机联锁、列控、无线闭塞以及临时限速等多个安全苛求系统大都采用二乘二取二架构形式[2-3]。

为了保证安全苛求系统安全可靠的运转，对系统性能的分析和验证显得尤为重要。与传统的测试手段不同，形式化方法具有的数学基础，为系统的模型设计和验证提供了严格验证手段，形式化方法是一种新型严格意义上的验证方法，被IEC50128等国际标准或者行业规范推荐使用。形式化方法在列车控制安全苛求系统中得到了广泛的应用[4-9]。

安全苛求系统的模式转换存在复杂性，标签转移系统(LTS)在处理系统复杂行为中具有良好的验证功能，并在安全通信协议RSSP-1协议[10]，ERTMS/ETCS需求[11]分析与实现中得到了应用。针对二乘二取二安全苛求系统，使用标签转移系统进行建模分析，验证了系统的安全使用性。

2 二乘二取二的安全苛求系统

2.1 二乘二取二安全苛求系统架构

二乘二取二系统由两个功能完全相同的系统A系和B系组成，每个系统是二取二结构，A系和B系两个系统构成双机热备冗余模式。两个系统通过硬件配置区分A系或者B系。正常工作时，一系为主控，控制整个系统的输出；另一系为备用，随时准备替换出现问题的主控系统。为了实现人为选择控制功能，系统中配置了切换控制手柄，手柄有3个状态：A系主控、B系主控或者自动模式。不需要人工干预时手柄指向自动位置。人工也可以通过旋转手柄，强制将A系或者B系升级为主控状态

任意一个系统A系或者B系，包括两个CPU(一个主CPU，一个从CPU)用以实现二取二比较；两块CAN通信板，与外部采集驱动板FIMO和FIMI系统进行采集驱动信息交互；若干外部以太网通信板，用以和其他安全苛求系统实现安全控制信息，系统实时状态等关键信息交互；为了减少系统的共模错误，比较板作为第三方硬件比较器，实现主从CPU板上总线数据的实时校核[6]。整个安全苛求系统结构如图1所示。

图1 二乘二取二系统构成

2.2 二乘二取二系统工作模式

二乘二取二系统的工作方式采用双系互为主、备，能实现“无扰”自动切换，且人工手动切换优先的主备冗余方式[12-14]。

系统有主控、备用、初始化、联机和离线5种稳定状态[15]。

主控状态是指计算机系统具有控制权的工作状态，此种状态只有在确认另一系不是主控状态且本系拥有控制权时才能发生。具备主控状态的系统称为主系。

备用状态是指计算机系统通过同步相关数据，已使本身数据状态与主系的对应状态一致，并保持一致的输出。具备主控状态的系统称为备系。备系应具备随时以“无扰”切换方式接替主机工作的能力，切换与状态的转换必须严格遵循安全、可靠、合理的切换原则，一般以主系“离线”为先决条件。

初始化状态是指计算机系统从关机到上电启动，或从其他状态复位重启时初始阶段的工作状态。通常只有人工操作或意外断电等某些导致复位启动的故障，可使计算机系统进入初始化状态。

联机状态是指本系与另一处于主控状态的系统建立同步传输链接，将关键状态数据交互，复制同步环境的工作状态。

离线状态也称脱机状态，是指计算机系统已退出上述4种正常工作状态以外的其他状态。通常计算机系统因发现故障、失步而自动退出，手柄切换强制退出正常所在状态都导致其进入离线状态；运行中关机、掉电、程序死锁等原因导致的死机状态也属于离线状态。

上述5种状态中，主控状态、同步状态和离线状态是长期稳定工作状态。联机状态为短暂过渡状态；初始化状态由于其系统状态标志在建立中，可以认为是离线状态的一种特殊形式。

A系和B系的两系统所有5种状态的组合关系如表1所示。由表1可以看出，25种状态组合中，只有12种情况是允许出现的。

表1 二乘二取二系统转换关系

2.3 系统工作模式转换处理机制

系统程序根据切换手柄的状态、系统各自的工作状态并配合检查对方系的工作状态来处理和实现工作模式的无缝转换。系统工作模式切换机制如图2所示。

图2 系统工作模式转换流程

当手柄处于自动位置，系统设置为自动模式。系统启动上电后进入初始化状态。初始化状态进行系统状态检查，具体包括本系和另系状态继电器接点闭合情况。如果初始化检查不通过不能进入主控状态。如果上电时手柄在手动位置，则手柄指向的一系在初始化检查正常后进入主控状态，另一系不需要对状态继电器进行检查，维持离线状态。

系统程序正常工作后，需要进行周期检查，即每个运行周期要检测手柄和两系的状态继电器的状态和系统关键变量状态，以此决定本系下一周期的工作状态。其中，检查关键变量包括严重错误标志、主从CPU板的输出比较结果、两系间的输入输出比较结果、两系间的通信状态、通过ETH板卡连接的其他安全苛求系统的通信状态等因素。系统在周期检查失败后将进入离线状态。

系统正常运行时，一系主控，另一系备用。除了在初始化阶段系统通过检查后可以直接升为主控状态的情况，在正常运行中，系统只能从备用状态进入主控，且前提是确认原主系已离线。另外，系统只能从离线状态进入联机状态，只能从联机状态进入备用状态。

联机状态为过渡状态。本系向成为主控状态的另一系联机时，首先向主系发送申请，在收到主系回复的同步状态信息后，用其初始化本系程序的变量数据，当本系的输出与主系比较结果一致时两系同步，本系变为备用状态。如果未能收到回复的状态同步信息或者与主系输出不一致，则本系离线，延迟一段时间后重新进行联机操作。

3 系统逻辑的模型验证

3.1 转移标签系统(LTS)

LTS转移标签系统由一系列过程P组成，P可以用四元素，描述，其中

(1)Q是由非空状态集合；

(2)A=α(P)∪{τ}是有限的标签集，其中α(P)表示字母表P，τ为包括内部行为，不为外部环境所知；

(3)Λ⊆Q×A×Q代表一个转移关系；

(4)q0∈Q，是Q的初始状态。

LTSA软件是一个系统行为分析验证工具，模拟系统交互行为，检查系统并发行为是否满足系统需求。LTSA软件将系统行为描述成一系列交互状态机。每一个需求被描述成一个LTS组件，包括组件可能达到的所有状态和转移情况。LTSA软件通过组件可达性分析，遍历搜索组件的错误行为。LTSA软件支持过程代数定义，如有限状态过程FSP语言的组件行为描述，可以将相应的FSP需求组件行为图形化显示。

3.2 系统模式转换建模

根据图2的平台逻辑处理，对于一系的字母集定义如下

A={inichk，inisysOK，inisysBad，cycchk，cycsysOK，cycsysBad，reInit，othOffline，othMainControl，checksw，checkOth，standBy，swtoself，swtoOth，swtoAuto，swAuto，swSelf，swOth}

动作列表如表2所示，系统交互行为使用FSP语言建模如下

S=S1，

S1=(inichk->inisysOK->checksw->swAuto->checkOth->othOffline->S2

|inichk->inisysOK->checksw->swSelf->S2

|inichk->inisysOK->checksw->swOth->S3

|inichk->inisysOK->checksw->swAuto->checkOth->othMainControl->S4

|inichk->inisysBad->S1)，

S2=(inichk->inisysBad->checksw->swAuto->S3

|reInit->S1)，

S3=(swtoself->checkOth->othOffline->S2

|checksw->swAuto->cycchk->cycsysOK->S4

|checksw->swOth->S3)，

S4=(checksw->swAuto->checkOth->othMainControl->standBy->S5

|checksw->swAuto->cycchk->cycsysBad->S3

|swtoOth->swOth->S3

|reInit->S1)，

S5=(checksw->swAuto->cycchk->cycsysBad->S3

|swtoOth->S3

|checksw->swAuto->checkOth->othOffline->S2

|swtoSelf->swSelf->checkOth->othOffline->S2).

借助LTSA软件，系统模式转换的LTS模型转换状态如图3所示。图3表明系统模式转换逻辑的状态存在47个临时状态，交互过程中不存在死锁现象。

图3 系统模式转换LTS模型

操作描述操作描述inichk本系初始化检查checksw检查手柄状态inisysOK本系初始检查正常checkOth本系检查另一系的状态inisysBad本系初始检查失败standBy本系联机另一系cycchk本系周期检查swtoself手柄转向本系cycsysOK本系周期检查正常swtoOth手柄转向另一系cycsysBad本系周期检查失败swtoAuto手柄转向自动位置reInit本系重新初始化swAuto手柄处于自动位置othOffline另一系处于离线状态swSelf手柄处于指向本系的位置othMainControl另一系处于主控状态swOth手柄处于指向另系的位置

4 安全性分析

在系统模式转换逻辑中，如果某些错误发生，应该按照故障-安全原则，状态需要导向安全侧。如下系统行为在模式转换过程中不允许发生。

(1)本系初始化检查错误本系不能联机另一系。

(2)本系周期巡检错误，不能联机另一系。

通过LTSA软件的安全属性进行检验。威胁行为的安全属性由FSP语言建模如下

propertySafety=Safe，

Safe=(inisysBad->standBy->Safe

|cycsysBad->standBy->Safe).

使用LTSA软件验证属性结果如图4所示。图4中状态标签‘-1’代表错误状态。系统安全属性(1)和系统安全属性(2)都满足安全原则。

图4 平台模式转换安全属性LTA模型

5 形式化验证应用和性能分析

LTS形式化方式应用在二乘二取二系统，克服了异常错误，概念歧义等问题。为了便于对比，安全苛求平台分别使用上述推荐方法和传统人工验证方法进行开发测试，最后软件通过C语言实现并在DOS操作系统实现。

两个开发小组独立使用LTS方法和人工验证方法的记录如表3所示。记录项包括两种方法设计的程序缺陷数目，系统完成费时量。从表3可以看出，采用LTS模型方法产生的程序缺陷数目比传统人工方法少64%。同时，系统开发工作量节省29%。结果表明，LTS方法为系统开发者缩短了设计实现周期并提高了开发质量。

表3 验证方法结果对比

6 结语

本文介绍了一种基于LTS模型验证方法，并在二乘二取二平台的实际开发工程应用。根据平台的交互行为和安全属性建立的LTS模型，通过LTSA软件进行了验证，验证结果对于实时安全苛求系统的设计者和开发者具有极大的帮助。

[1] 郭玉华.借鉴ETCS完善CTCS技术规范体系的研究[J].铁道标准设计，2016，60(10)：136-140.

[2] WANG X， Ma L C H， Tang T. Study on formal modeling and verification of safety computer platform[J]. Advances in Mechanical Engineering， 2016，8(5)：1-13.

[3] 季忠红，王俊高，冯浩楠.基于二取二平台的计算机联锁软件异构性能分析及设计[J].铁道标准设计，2016，60(11)：135-138.

[4] 曹源，唐涛，徐田华，等.形式化方法在列车运行控制系统中的应用[J].交通运输工程学报，2010，10(1)：112-126.

[5] 胡雪莲，陶彩霞.基于MSC与UPPAAL的列控系统等级转换场景形式化验证[J].铁道标准设计，2015，59(2)：122-127.

[6] 徐世泽，肖蒙.基于Timed RAISE的高速列车RBC切换协议形式化建模及验证[J].铁道标准设计，2015，59(6)：138-144.

[7] 郭志良，郜春海，马连川，等.基于时间自动机模型的安全计算机平台的形式化验证[J].铁道学报，2011，33(6)：68-73.

[8] 吕继东，唐涛，燕飞，等.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证[J].铁道学报，2009，32(3)：59-64.

[9] 彭大天，步兵.基于UPPAAL的FAO系统典型运营场景建模与验证[J].铁道学报，2013，35(6)：65-71.

[10] MEI M， XU ZH. W.， WANG X.， et al. Model checking-based safety verification for railway signal safety protocol-I[J]. Int. J. Computer Applications in Technology， 2013，46(3)：195-202.

[11] Mohamed Ghazel. Formalizing a subset of ERTMS/ETCS specifications for verification purposes[J]. Transportation Research Part C， 2014，42:60-75.

[12] 刚建雷，胡燕来，窦道飞，等.二乘二取二安全控制平台开发[J].铁道通信信号，2012，48(6)：1-4.

[13] 张新明，刘海祥，赵永清.二取二制式计算机联锁系统中的通信技术[J].中国铁道科学，2005，26(5)：96-100.

[14] 张萍，赵阳.TYJL-III型计算机联锁系统研究[J].中国铁路,2013(11)：21-26.

[15] 段武.计算机联锁系统[M].北京：中国铁道出版社，2015.