Timed RAISE方法在列控系统等级转换场景中的应用研究

丁春平,陈永刚

(兰州交通大学自动化与电气工程学院,兰州 730070)

Timed RAISE方法在列控系统等级转换场景中的应用研究

丁春平,陈永刚

(兰州交通大学自动化与电气工程学院,兰州 730070)

高速铁路列车运行控制系统是一个复杂的实时性系统,结合其实际特点,将域方法作为系统描述的切入。通过对模型检验和定理证明两种验证方法的分析比较,提出使用基于定理证明的时间化工业软件工程的严格方法Timed RAISE形式化方法对等级转换(CTCS-2级至CTCS-3级)场景进行描述,并对其场景交互一致性和实时性进行验证,结果表明该场景不会出现场景交互一致性错误,也不会违反时间的约束。

高速铁路； Timed RAISE； CTCS；等级转换场景；实时性；场景交互一致性

高速铁路是经济社会发展的必然趋势，它具有安全性高、速度快等特点[1]。随着计算机、通信、控制技术等先进技术的广泛应用以及列车速度和密度的不断提高，对系统的安全性和可靠性要求也越来越高。为了保证列车安全运行、降低事故发生率，需要高可靠性、高安全性的列车运行控制系统作为保障[2]。根据中国铁路列车特性、运行速度、线路条件等运输需求，将中国列车运行控制系统CTCS(Chinese Train Control System)分为CTCS-0级(简称C0)-CTCS-4级(简称C4)共5个等级[3]。C3级列车运行控制系统有效提高了列车的运营效率，该系统主要包含14个场景文件：注册与启动、注销、等级转换、RBC切换等[4]。本文对等级转换(C2-C3)场景的条件及转换过程做了详述，并基于域+Timed RAISE对其进行初步描述、验证和分析。

1 C2-C3等级转换原理

1.1 转换前准备事项

在等级转换前需要对标志牌、转换点和确认区进行设置[5]。其中标志牌设置包含通信连接标志牌、等级转换标志牌的设置。转换点设置包括GSM-R连接点(GRE)、RBC连接点(RE)、转换预告点(LTA)、转换执行点(LTO)、转换取消点的设置。等级转换确认区为等级转换边界点前一定距离(列车以最高速度运行至转换点边界约5 s的时间)和等级转换后列车运行5 s的区域[6]。图1所示即为C2-C3级间转换过程中应答器布置和确认区设置。

图1 C2-C3中应答器布置和确认区设置

1.2 C2-C3级间转换过程

列车由C2转换到C3控车前，需完成车载电台注册到GSM-R无线网络、ATP与RBC建立通信等信息。如果在C2-C3转换边界不具备等级转换条件，则列车继续按C2控车，直至具备C3控车条件后，列车自动转入C3控车。一个典型的C2-C3控车的流程有以下6步[7-8]。

(1)车载设备在40 s内检测并注册到GSM-R网络并建立可靠连接。

(2)车载设备与GSM-R网络建立连接后，列车经过RBC连接应答器组后，发送建立通信会话命令。系统版本信息通过RBC发送给车载设备，由车载设备检查该版本信息的兼容性，若不兼容，则停止会话。

(3)由RBC发送位置报告和MA参数信息给车载设备。车载设备收到信息后，把列车位置信息、当前控制等级信息发送给RBC。RBC收到信息后，发送配置参数给车载并给出确认信息。

(4)列车通过LTA后，ATP向RBC发送列车数据信息并报告列车位置。RBC计算出MA参数后，将MA和等级转换命令发送给车载设备。

(5)当列车接近C2-C3级间转换LTO时，司机对将要进行的转换等级确认。

(6)列车头部经过LTO后ATP自动转到C3控车。

2 Timed RAISE

2.1 形式化方法概述

在系统验证初期，为了发现大量而又明显的设计错误，对系统特性进行验证一般使用仿真和测试的方法。然而，这两种方法并不是万能的，它们无法检查系统设计中存在的精微深奥而又繁琐的错误。对于复杂系统，如果仿真和测试案例不能被正确地选取，很难对复杂系统的运行状态和执行路径进行穷尽的遍历，从而会给系统安全带来潜在的危险因素[9]。IEC62279：2002(《铁路应用-通信、信号和处理系统-铁路控制和防护系统软件》)中提出：“在软件安全度完善等级为4级时，软件需求规格说明书定义、软件设计和实施、验证和测试等过程中，强力推荐使用形式化方法进行描述和设计，对于在软件验证和测试时，强力推荐的形式化证明技术[10]。”同时IEC61508中也提出了：“在系统的安全完善度等级为4级的时候，强烈推荐利用形式化证明方法对系统进行验证[11]。”

模型检验和定理证明作为形式化验证方法各有优势和不足[12]。形式化验证方法模型检验的主要对象是有限状态系统。验证流程是：首先对系统进行描述，最好选用能够对系统描述详尽的形式化语言；接着对系统形式化模型进行遍历，选用能够实现对系统运行状态和执行路径穷尽遍历的算法；最后分析判定系统某种特性的要求能否被实现。当判定系统某种特性的要求不被满足时，为了方便定位错误的发生，形式化验证方法模型检验会给出反例[13]。在基于定理证明的形式化方法中，首先定义了一种特殊的数学逻辑系统，接着将期望验证的系统和相关重要特性用一系列公理和推理规则组成的数学逻辑表示，最后以系统的公理为基础，使用推理规则一步一步推导出系统所期望的性质[14-15]。

表1所示为常用形式化方法的总结[16]。

表1 形式化方法比较总结

注：◆表示能对此性质验证；◆◆表示适合对此性质验证

从表1中可看出：某种单一的方法只适应于描述系统的少数特性，无法全面准确地描述和验证复杂系统。当系统复杂、多任务并发运行或多子系统时，模型检验方法将会产生状态空间爆炸问题，然而，基于定理证明的形式化方法却与模型检验的形式化方法不同。具有无限状态空间的复杂系统可以用定理证明的形式化方法对其分析和验证，这种形式化验证方法能够对某个数域的特性实现完全验证主要是由于它不依赖于参数取值范围。

模块性是RAISE方法的一个特点，可以通过模块来规范值、变量、类型等各类实体。而且RAISE也具并发性，易于对进程间的相互关系以及进程间的并发性进行研究。RAISE方法吸取了OZ、CSP的精华，但无法描述系统的时间特性。将时间约束条件加入RAISE方法中形成Timed RAISE，因此，Timed RAISE能够对具有实时性的复杂系统进行比较全面的描述。

2.2 Timed RAISE

Timed RAISE方法，即在RSL语言中引入了一个表示时间的类型和一个描述延迟的等待表达式。由于RSL语言自身有着结构完善的语法、语义以及相应的支持工具，所以这种扩充必须是最小化的，即不能破坏RSL语言的原有结构[17]。

(1)Time类型的添加

在RSL语言中扩充了如下与时间有关的描述机制。

Type

Time //定义时间类型Time

Value

System:Unit→Time //定义函数System

其中，Time 数据类型主要用于说明与时间相关的变量。它被定为一个非负实值时，可以作为进行连续计时的系统时钟。定为一个自然数时，可作为系统计数器。表2是对时间表达式操作符的相关定义。

表2 操作符定义

+、-操作作用在两个时间类型的值上返回一个时间类型的值；而×、÷(整除)操作将一个时间类型的值与一个整数相运算，主要用于实现对时间的翻倍或是减半；此外还有4个比较操作符(﹥、≧、﹤、≦)，其优先级顺序与RSL中的规定一致。

在RAISE的扩展中，函数System主要用于获取系统时间，假设该函数的执行不消耗任何时间；Time时间类型实质上是RSL固有类型Real的一个子类型，所以尽管定义了这样一个Time时间类型和作用在其上的8种操作，却不会改变RSL原有的语义结构，这种扩充符合最小化的要求。此扩充的语法规范为：

type_expr ::=Unit | Bool | Int | Nat | Real |

Text | Char | Time |…

在对RSL语言进行了如上扩充后可解决信息传输中的等待时间问题和操作执行时间问题。前者即超时问题，用当前时间值减去开始等待时间值，如若结果超过某个设定值，即认为出现超时问题，从而执行对应的超时出错处理；后者即数据准备和传输时间问题，该类问题要求一个操作必须在限定的时间值范围内完成，这一点可以通过比较操作执行前后的系统时间值来准确描述。

(2)wait表达式的添加

为了保证RSL语言扩充后的广谱性不被弱化，从而引入wait r表达式。整个wait r表达式的运算值为Unit，r是一个Time时间类型。运算出r的值之后，wait r表达式不做任何事情延时r个时间单位。

引入wait r表达式后，超时机制描述如下：

Class=

value Operation Unit → Unit

time_lim it Time

axiom

Operation( ) ≡

…… //具体操作

Wait time_lim it

…… //超时处理

end

在RSL语言中引入一个表示时间的类型和一个描述延迟的等待表达式后就形成Timed RAISE方法，其对应语言用TRSL表示。引入wait r表达式之后，扩充后的RSL语言广谱性就不会被弱化，然而，这种扩充可能会给RAISE原有确定语义带来不确定性。因此，对于引入wait r表达式的RAISE方法的语法、语义，有必要重新定义和讨论，在这里不再详述。

3 C2-C3的描述验证

一些指标或量化参数常用来反映列车运行控制系统的性能，而这些参数基本上存在于某个场景或过程中，本文以等级转换(C2-C3)场景为例，对域的场景交互一致性和实时性进行具体的描述验证。

3.1 域模型建立

C2-C3级间转换场景中的时间约束[4]：

(1)GSM-R无线网络注册时间40 s；

(2)车载与无线闭塞中心的连接时间10 s；

(3)在ATP与RBC建立通信后，RBC与车载设备间必要信息的传输时间预估为20 s；

(4)进行等级转换前司机的确认时间为5 s。

仅为说明该方法的有效性，对该场景进行以下简化：

①在该场景中，仅考虑车载ATP和RBC；

②认为所有的延时或人为失误都不存在，也就是说不需考虑司机确认的时间约束；

③转换中系统的所有设备都不发生故障；

④GSM-R中的所有通信过程最终都是可以完成的，对于上述(1)、(2)这两个时间约束可以通过对GSM-R随机时间的定义来满足；

⑤上述(3)的时间约束在该场景中是一主要的不可忽略的考核指标。

根据域的定义，针对C2-C3转换场景，提出4个基本元素：输入(I)、输出(O)、函数(F)以及特性(T)。如图2所示，ATP的等级、轨道电路区间占用等，在域函数的作用下，实现状态的变换和操作，最终实现输出。根据前述转换过程，考虑主要时间约束条件，给出C2-C3状态转移如图3所示。

图2 等级转换(C2-C3)场景域模型

图3 等级转换(C2-C3)场景状态转移

3.2 域的相关描述

根据等级转换(C2-C3)域模型以及状态转移图，对其关键进行如下描述。

(1)输入(I)：车载设备初始状态A0，RBC初始状态R0，与此同时，初态时信道中不存在已经传输的信息，A0到R1转移时间为0。

(2)输出(O)：车载设备最终状态A3，RBC最终状态R2。

(3)函数(F)：即图5所示的状态转移图。车载设备初始状态A0、RBC初始状态R0，通过域函数F的作用最终转换为车载设备最终状态A3、RBC最终状态R2。

(4)特性(T)：实时性和交互一致性。

对等级转换(C2-C3)场景域模型的RSL描述主要有车载设备、RBC以及消息集三个模块的状态描述。限于篇幅，仅对车载设备A0状态和交互过程中涉及的消息集为例做以简单说明。

车载设备A0状态的RSL描述：

Send_CallRBC∶ATP×GNET→ATP×GNET

/*向RBC发送建立通信会话命令*/

Send_CallRBC(a，ch)≡

/*该式中”≡”表示恒等函数*/

wait NetworkRegDelay;

/*考虑网络注册时间*/

ATPSend(CallRBC(r));

/*ATP发送呼叫RBC信息*/

wait ComDelay

/*考虑传输延迟时间*/

wait BuildLinkDelay;

/*ATP与RBC建立连接，需等待一定延迟*/ change_state(A1);

/*ATP的下一个状态为A1状态*/

等级转换(C2-C3)域模型消息集的RSL描述：

Message==

CallRBC(r)|Config(a)|MA(a)|

Pos(a)Pos&MAValue(a)|CallRBCAck(a)|

MAReq(r)|LevelTrain(a)|Level&Mode(a)

|nil|error

/*在切换过程中，涉及到车载配置参数、位置参数、MA请求参数信息、列车等级、列车模式、空包、错误包等消息集*/

3.3 验证

在等级转换 (C2-C3) 场景中，同时对场景实时性和交互一致性问题进行验证。整个验证过程的简易流程如图4所示。

图4 验证流程

(1)场景交互一致性axiom模型

axiom

[C2-C3_consistent]

/*C2-C3交互一致性Timed RAISE描述*/

∀ a∶ATP， r∶RBC， ch∶GNET •

/*a代表ATP， r代表RBC， ch代表GNET • */

ATP_state(a)=A0 ^ RBC_state(r)=R0

/* ATP、RBC初始状态分别为A0、R0*/

^RBCGet(r， ch)=nil^ATPGet(a，ch)=nil ^ TimePass (A0， R1)=0

/*初态时信道中不存在已经传输的信息，A0到R1转移时间为0*/

⟹let (a′， r′,ch′)=run (a， r， ch) in

/*run( )是一个遍历的函数*/

ATP_state(a′)=Aok ^

/*在遍历条件下，达到ATP最终态Aok*/

RBC_state(r′)=Rok ^

/*在遍历条件下，达到RBC最终态Rok*/

TimePass(R2， Rok)﹤=20

/*ATP向RBC发送位置报告的时间为20s*/

end

(2)实时性axiom模型

axiom

[TimeConstraininLevelTrains]

/*C2-C3实时性描述*/

TimePass(R1， Rok)=Time(R1)+Time(A1)+Time(R2)+Time(A3)

/*建立通信会话后，RBC与车载设备之间进行必要信息的传输时间*/

在文献[18]中重点推荐了9种证明方式：Equivalence(等价)、Inference(推演)、Lemma(引理)、Conclusion(结论)、Assumption(假设)、Side(分支)、Axiom(公理)、Relevance(关联)以及Commented(非正式)[18]。在等级转换(C2-C3)特性验证的过程中，主要使用推断规则(inference rules)和等价规则(equivalence rules)对实时性和场景交互一致性同时进行验证，当且仅当两种验证结果都为true时，方可认为该场景没有发生交互一致性的错误。通过验证，结果表明该场景不会出现交互一致性错误，也不会违反时间的约束。

4 结论

高速铁路列车运行控制系统是一个复杂的实时性系统，结合其实际特点，将域方法作为系统描述的切入。随之使用Timed RAISE形式化方法对实时性较强的等级转换(C2-C3)场景进行描述和验证，结果表明列车在等级转换(C2-C3级)场景中，即使无线网络GSM-R的随机延迟会很大程度地影响场景的实时性，但依然能够实现规范中等级转换作为(C2-C3级)场景的交互一致性和实时性要求。此外，将域方法和Timed RAISE结合推广用于具有混成性、实时性、分布性的列控系统，可以实现对列控系统的整体性能验证。

[1]李学伟.高速铁路概论[M].北京:中国铁道出版社，2010:10-14.

[2]车玉龙，苏宏升.基于蒙特卡罗的CTCS-3级列控系统单元重要度分析[J].铁道标准设计，2013(8):125-128.

[3]陈令仪.故障注入技术在CTCS-3级列控系统仿真测试平台中的应用研究[D].北京:北京交通大学，2011.

[4]唐涛.列车运行控制系统[M].北京:中国铁道出版社，2012:168-178.

[5]康仁伟，王俊峰，吕继东.基于UPPAAL的高铁列控系统等级转换过程建模与验证[J].北京交通大学学报，2012，36(6):63-68.

[6]铁道部科技技术司.科技运[2008]144号CTCS-3级列控系统应答器应用原则[S].北京：铁道部科学技术司，2008.

[7]程忆佳.基于等级转换场景的CTCS-3级列控数据完备性分析[D].北京:北京交通大学，2011.

[8]康仁伟，王俊峰，吕继东.基于UPPAAL的高铁列控系统等级转换过程建模与验证[J].铁道标准设计，2012(6):63-68.

[9]徐田华.概率模型检验及其在列车运行控制系统中的应用[D].北京：北京交通大学博士后出站报告，2007.

[10]IEC.IEC62279：2002. Railwayapplications-Communications， signa-

ling and processing systems-Software for railway control and protection systems[S]. IEC.2002.

[11]IEC.IEC61508：2005. Functional Safety of Electrical/ Electronic/Programmable Electronic Safety-Related Systems[S]. IEC.2005.

[12]肖健宇，张德运，陈海诊，等.模型检测与定理证明相结合开发并验证高可信嵌入式软件[J].吉林大学学报：工学版，2005，35(5):531-537.

[13]宋海锋.基于模型检验的RBC子系统测试分析方法研究[D].北京:北京交通大学，2014.

[14]郑红军，张乃孝.软件开发中的形式化方法[J].计算机科学，1997，24(6):90-96.

[15]谢雨飞.列控系统需求规范形式化建模与验证方法研究[D].北京：北京交通大学，2012.

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

[17]Xia Yong， Chris George. An operational semantics for timed RAISE[C]∥FM’99-Formal Methods. Springer Berlin/ Heidelberg, 1999：715-730.

[18]C.George， S Prehn. The RAISE Justification Handbook[M]. LACOS/CRI/DOC/7/V5.1994.

Application of Timed RAISE Method in Level Conversion Scene of Train Control System

DING Chun-ping, CHEN Yong-gang

(School of Automation and Electrical Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China)

The high-speed railway train control system is a complex real-time system. In the light of the actual features of the system, the domain method is employed for system modeling. With the analysis and comparison of model verification and theorem proving, the theorem-proving-based Timed RAISE (Timed Rigorous Approach to Industrial Software Engineering) is recommended to describe level transition scene (CTCS-2 to CTCS-3) and verify the scene interaction consistency and real-time capability. The results show that this scene will not cause errors in scene interactive consistency, nor violate time constraints.

High-speed railway； Timed RAISE； CTCS； Level transformation scene; Real-time capability； Scene interaction consistency

2014-11-17；

2014-12-17

国家自然科学基金地区项目(61164101)

丁春平(1989—)，女，硕士研究生，E-mail:dingchunping_1@163.com；陈永刚(1972—)，男，副教授，硕士研究生导师，主要研究方向:交通信息工程及控制。

1004-2954(2015)08-0164-05

U283

A

10.13238/j.issn.1004-2954.2015.08.035