近年来，随着我国铁路运行控制系统（CTCS）的高速发展，速度在200 km/h以上高速列车的CTCS-2与CTCS-3级列控系统已日臻完善，对于提高列车运行自动化水平，保证行车安全发挥了重要作用。据统计，我国铁路运营里程中普速线路（既有线）占总里程数的70%，而既有线对应的CTCS-0级列控系统存在诸多安全问题。为此，铁路总公司组织开展了“ CTCS-1级列控系统关键技术的研究”工作^[1]。

CTCS-1级列控系统由车载设备和地面设备构成。其中，车载设备包括车载安全计算机、轨道电路信息接收单元、无线通信单元、应答器信息接收单元等；地面设备包括区域列控数据中心（RDC，Regional Data Center）、轨道电路、无线通信接口设备以及应答器等^[1]。RDC作为CTCS-1级列控系统的地面核心设备，实时为列车提供行车数据、进路信息、临时限速信息。RDC数据的正确性对列车运行具有极其重要的意义。目前，RDC基础数据主要根据工程数据表、CAD设计图进行纯手工编制，编制完成后需要人工校核比对，数据的正确性难以保证。因此，亟需一种对RDC数据进行自动化验证的方法。

目前，针对列控系统数据验证的研究较少，并没有系统化的研究成果。文献[2-3]分析了列控系统对数据的安全苛求，从数据管理的角度提出提升数据准确性的方法。Michael Huber等人^[4]联合开发了工具gdlSMV直接读取联锁地理数据并通过符号模型检查内置算法对数据进行自动化验证，但该方法建立在程序级别，很难验证数据的耦合性问题。文献[5]对基于通信的列车运行控制系统（CBTC）静态数据先用SAT方法进行处理，然后提出采用基于通信顺序进程（CSP，Communicating Sequential Processes）的方法对数据进行验证，并以地面电子单元（LEU）码位表中的数据是否与联锁逻辑匹配为例，结合具体场景来说明该方法的可行性，但该研究过程并未对数据实体应满足的规则进行归纳和模型验证。因此，本文在对RDC静态数据（简称：RDC数据）内容和约束条件进行归纳的基础上，以车站轨道区段数据为例，归纳出实体数据应满足的规则，将数据验证规则加入数据验证流程，利用CSP形式化方法对RDC数据的验证流程进行建模，并利用验证工具—RroB对该模型的死锁、活锁、确定性、功能性特性进行自动化验证，验证结果表明该模型可应用于RDC数据验证，为自动化数据验证工具的开发奠定了基础。

1   RDC静态数据分析

1.1   RDC数据总结

RDC包含独立的线路数据库，用于存储当前RDC所管辖范围内全部线路的静态数据。RDC根据当前列车的位置信息、轨道电路占用情况从数据库中读取线路数据并按照一定的规则组织数据，同时结合车站联锁发来的进路信息与临时限速服务器发来的临时限速信息，通过无线通信方式发送给车载设备。RDC数据库中线路数据包括：轨道区段数据、道岔数据、应答器数据、线路限速数据、坡度数据以及进路数据。

1.2   RDC数据约束条件分析

RDC数据库中的每个数据都并非单独的个体，都有其空间物理意义，这些数据共同构成了整个线路的拓扑结构。数据约束条件即数据应满足的条件，在数据验证过程中应该围绕数据的约束条件进行验证。通过对RDC数据进行分析，归纳出以下几个方面的数据约束条件。

1.2.1   属性域值条件

RDC数据库中的数据表现形式为数据表格，每个数据对象都填写在相应的数据表中，每个数据对象都有若干个实体属性，比如取值范围、精度、数据格式等。

1.2.2   拓扑约束条件

数据间的拓扑关系指空间上各个数据描述对象间的相邻和连接关系。空间的地理特性通过数据的公里标、道岔定反位等信息来体现。拓扑约束条件分为以下3个方面。

（1）映射关系

映射关系指轨旁设备映射在轨道区段上的位置关系。轨旁设备的属性字段中包含了所属轨道区段一项，因此轨旁设备的位置应在其所在区段的始末端点公里标之间。除了轨旁设备之外，道岔的岔尖里程也应在其所在轨道区段的范围内。

（2）关联关系

RDC数据在对线路和轨旁设备进行描述时，各个数据并不是单独存在的，具有一定的关联性。一个数据项的属性值可以推导出另外一个与之相关联的数据属性值。

（3）连续关系

连续关系表现在两个方面：（1）各个数据索引号的连续关系；（2）相邻区段的里程数连续，符合此连续关系的数据有：轨道区段、线路限速、坡度信息。

综上所述，RDC数据库所包含的静态数据以及数据之间的关系可用如图 1所示类图表示。

图  1  RDC静态数据类图

下载: 全尺寸图片 幻灯片

2   数据约束规则提取

RDC实体数据应满足的约束规则是基于《列车运行监控装置（LKJ）数据文件编制规范（V1.0）》 ^[6]和RDC静态数据库的数据结构以及数据编制经验得到，通过对各个数据字段的分析整理可得到完备的数据验证规则。

以车站轨道区段数据为例，轨道区段Section数据是一个十一元组，可以描述为 < Seg_index, Seg_sigpointtype, Seg_startloc, Seg_sigtype, Seg_endloc, Seg_frequency, Seg_length, Seg_upordown, Seg_ swinum, Seg_swiloc>，分别代表区段索引号、信号点类型、起点公里标、信号机类型、终点公里标、轨道区段载频、轨道区段长度、线别、道岔数量、岔尖里程。车站轨道区段数据应满足的具体规则如下。

（1）区段索引号即为区段编号，应满足唯一性和连续性，即：

Seg_index ∈{1, 2, …，n}

Seg_index_i+1=Seg_index_i+1

（2）信号机类型和信号点类型只包含没有信号机、进站信号机、通过信号机、进路信号机、调车信号机、出站口、出站信号机、容许信号机、预告信号机9种类型，记为{1，2，3，4，5，6，7，8，9}。

（3）起点公里标和终点公里标的取值都为非负整数。

（4）线别只包含上行线和下行线2种类型，记为{0, 1}。

（5）在规则（3）和（4）满足的前提下，若线别为下行线情况，则终点公里标满足：

Seg_endloc>Seg_startloc

若线别为上行线，则终点公里标满足：

Seg_startloc>Seg_endloc

（6）道岔数量可能为0、1、2的3种类型，记为{0, 1, 2}。

（7）轨道区段载频包含0、1 700 Hz、2 000 Hz、2 300 Hz、2 600 Hz5种类型，分别记为{1, 2, 3, 4, 5}。

（8）岔尖里程数必须在起点公里标和终点公里标之间，即：

Seg_startlo<Seg_swiloc<Seg_endloc

（9）在规则（3）和（4）满足的前提下，若为下行线则区段长度为终点和起点公里标之差，即：

Seg_lenght<Seg_endloc<Seg_startlo

若为上行线则区段长度为起点和终点公里标之差，即：

Seg_lenght=Seg_startlo–Seg_endloc

（10）相邻轨道区段公里标连续，即：

Seg_startlo_i+1=Seg_endloc_i

（11）在规则（4）和（7）满足的前提下，下行线载频只包含0、1 700 Hz和2 300 Hz3种情况，上行线载频只包含0、2 000 Hz和2 600 Hz3种情况。

3   验证方法和思路

确立数据约束规则后，需将数据约束规则加入数据验证流程，并利用形式化方法CSP语义对数据验证流程建模并验证，以得到正确的数据验证流程。

3.1   CSP语义

CSP是一种针对并发系统的代数理论，该方法可以精确地描述由多进程构成的系统，进程内部通过消息交互来推动事件的发生和状态的转移。CSP语义模型具有可遍历所有事件和状态的特点，可以完整地验证所有情况，因此本文采取该方法对数据验证流程进行建模。

进程（Process）是CSP方法的基本要素之一，其基本结构包括前缀进程、确定性选择、非确定性选择、递归4部分。

3.1.1   前缀进程

x → P或P=STOP，表示一个有限行为进程，进程名通常用大写字母表示，STOP代表终止进程，执行到该进程后不再进行任何操作。常用的前缀进程包括以下几种：

（1）事件前缀选择进程

（?x: → P），若A为一事件集合，即A⊆∑，则进程？x: → P(x)代表当执行任意动作x∈A时，下一动作执行进程P，执行后的状态为P(x)，即x为是否执行进程P的判断条件。

（2）输出前缀选择进程

（C!x : → P），其中C为进程间通信的通道，C!x : → P(x)表示在通道C上输出x后，执行进程P(x)。

（3）输入前缀选择进程

（C?x: → P），C为进程间通信的通道，A⊆∑，则进程C?x: → P(x)表示通过通道C接收输入x∈A后执行进程P(x)。

3.1.2   确定性选择进程

P □ Q表示由外界环境决定执行进程P或者Q。

3.1.3   非确定性选择进程

P ∏ Q表示该进程是任意的，不受外界环境影响，可选择P或者Q。

3.1.4   递归进程

递归是用短得多的记法来刻画重复的行为。若X和P代表进程，∂P表示P的字母表，P(X)代表进程X的卫式，即P(X)服从∂→X，若X为不可终止进程，则X=P(X)代表递归进程，可以表示无穷进程。

3.2   CSP语义建模和验证思路

采用CSP语义对RDC数据验证流程进行建模，首先需要将数据约束条件加入数据验证流程，本文将每个数据字段抽象为单独的进程，数据间的相互联系通过相应的通道进行信息交互来实现。由于CSP语义是一种抽象化描述方式，因此需要对规则进行管理和抽象化描述，建模和验证流程分为规则管理、建立模型、模型验证3个阶段，具体流程如图 2所示。

图  2  RDC数据验证流程建模与验证框图

下载: 全尺寸图片 幻灯片

3.3   规则管理

3.3.1   规则分类

根据本文1.2节中对约束条件的归纳总结，将规则（1）~（11）进行分类：属性域值、映射关系和关联关系规则针对的是单个数据字段应满足的属性规则和数据字段间的相互约束关系，在数据表中体现为横向数据验证；而连续关系体现的是同一数据字段相邻数据间的关系以及不同字段间的连续关系，在数据表中体现为纵向数据验证。因此将每个字段抽象为单独的进程，将规则分为横向验证和纵向验证，分别对不同的字段的验证流程进行建模，可以使得验证过程条理更加清晰。

3.3.2   规则抽象

为避免状态爆炸，CSP语义不可能分析验证对象具体的属性值，只能在不影响所验证规则的基础上将数据取值进行抽象，比如线别Seg_upordown字段的值只能为上行线0和下行线1，其他取值都不合法，因此将该字段取值抽象为upordown0、upordown1和upordownother3种类型，分别代表取值为下行线、上行线和错误类型。

3.4   CSP建模

将抽象后的数据约束规则加入数据验证流程，对每个字段的数据验证流程用CSP形式化方法进行描述，其具体建模过程如下。

3.4.1   属性域值、映射关系和关联关系CSP模型

以体现上述约束关系的典型字段——终点公里标为例对验证过程进行建模。终点公里标需满足的属性域值条件对应规则（3）, 需满足的映射关系和关联关系条件对应规则（4）。将规则（3）和（4）加入数据验证流程，即：

（1）终点公里标进程END向起点公里标进程START通过通道ch_E2S发送检查请求，START进程接收到请求后检查起点公里标是否满足规则，若起点公里标数据正确则START将起点公里标的值通过通道ch_E2S发送给END，反之进入错误进程ERROR，终止判断。

（2）END进程获得起点公里标的值后，通过通道ch_E2U向线别进程UORD发送检查线别数据请求，UORD收到请求后检查线别数据，若数据为upordown0或upordown1，分别代表下行线或上行线，说明数据正确进入下一进程E2或E3，若数据为upordownother，代表其他类型数据，说明线别数据错误，进入错误进程ERROR，终止判断。

（3）若线别数据为下行线数据，则UORD进程通过通道ch_U2E将线别数据发送给END进程，然后END进程接收总进程SECTION通过通道ch_SS2E发送来的检查终点公里标请求，若Seg_endloc>Seg_startloc，即endmorethanstart事件发生，说明终点公里标数据正确，递归到进程END，对终点公里标的验证流程结束；若endpointother事件发生，则说明数据错误，进入进程ERROR，终止判断。上行线情况与下行线类似，不再赘述。

用CSP语义对上述验证流程建模如下：

END=ch_E2S!checkstartpoint → ((startpoint1 → ch_E2S?startpointcorrect → E1) ∏ (startpointother → ch_E2S?startpointerror → ERROR))

E1=ch_S2E?startpointvalue → ch_E2U?checkupordown →((upordown1 → ch_U2E?upordowncorrect → E3) ∏ (upordown0→ch_U2E?upordowncorrect→E2)∏(upordownother → ch_U2E?upordownerror → ERROR))

E2=ch_U2E?upordownvalue → ch_SS2E?checkendpoint →((endmorethanstart → ch_E2SS!endpointcorrect → END) ∏ (endpointother → ch_E2SS!endpointerror → error))

E3= ch_U2E? upordownvalue→ ch_SS2E?→ checkendpoint→((endlessthanstart→ ch_E2SS!endpointcorrect→ END)∏(endpointother → ch_E2SS!endpointerror → ERROR))

ERROR=dataerror → ERROR

3.4.2   连续关系CSP模型

以体现连续关系的典型字段—区段索引号为例对验证过程建模。索引号Seg_index连续关系需满足规则（10），定义进程INDEX1代表Seg_index_i，进程INDEX2代表Seg_index_i+1，将规则（10）加入验证流程，即：

（1）检查Seg_index_i+1数据是否满足连续性，首先需要保证Seg_index_i取值正确，即INDEX2进程通过通道ch_SS2I2向INDEX1发送检查请求，若Seg_index_i取值正确则进入进程I1，反之进入错误进程ERROR。

（2）INDEX2通过通道ch_I12I2得到Seg_index_i的值后，接收总进程SECTION通过通道ch_SS2I2发送的检查命令，检查Seg_index_i+1是否满足等式Seg_index_i+1=Seg_index_i+1，若满足即事件i2equi1p1发生，即说明索引号数据正确，递归到进程INDEX2，反之说明数据错误，进入ERROR进程。

用CSP语义对上述验证流程建模如下：

INDEX2=ch_I22I1!checkindex1 → ((index1other →ch_I12I2?index1error → ERROR) ∏ (index11 → ch_I12I2?index1correct → I1))

I1=ch_I12I2?index1value → ch_SS2I2?checkindex2 →((i2equi1p1 → ch_I22SS!index2correct → INDEX2) ∏(index2other → ch_I22SS!index2error → ERROR))

3.5   模型验证

将CSP语义模型代码导入模型验证工具，并将数据约束规则用线性时序逻辑（LTL，Linear Temporal Logic）语句来刻画，将两部分共同作为ProB模型验证器的输入，对模型的正确性和有效性进行验证并对结果进行分析。若出现错误则可根据反例对错误进行定位和追踪，从而发现模型中的错误并进行修改和重验。

其他数据字段的建模过程与3.4节中示例类似，将所有数据字段的验证流程建模完成后，将各进程的CSP语义模型先转换为CSPM语言，即机器可读语言，将其加载到ProB平台^[8]对各模型进行检验，部分程序如下所示。

-- section

channel checkindex, checkstartpoint, checkupord own, length, startpointvalue, endpointvalue, upord ownvalue, …

INDEX=checkindex->((indexother->indexerror->ERROR)[](index1->indexcorrect->INDEX))

…

LENGTH=(checkstartpoint->((startpoint1->startpointcorrect->L1)[](startpointother->startpointerror->ERROR)))[](checkupordown-> ((u p o r d o w n0- > L5) [] (u p o r d o w n1- > L6) [](upordownother->upordownerror->ERROR)))

L1=startpointvalue->checkendpoint->checkupordown->((upordown0->upordowncorrect->L3)[](upordownother->upordownerror->ERROR)[] (upordown1->upordowncorrect->L4))

…

SECTION=INDEX|~|UPORDOWN|~|STARTP OINT|~|LENGTH|~|ENDPOINT|~|INDEX1|~|IN DEX2|~|ENDPOINT1|~|STARTPOINT2

MAIN=SECTION

ProB平台可自动验证模型的死锁、活锁和确定性断言。模型验证主要从以下几个方面进行。

（1）死锁

死锁指系统处于某一状态时，一直处于等待状态，无法跳转到下一状态，从而导致系统进程无法继续。

（2）活锁

活锁指进程中存在死循环，该现象会导致系统中其他功能无法得到验证并使系统部分功能缺失。

（3）确定性

确定性指对于所建模型各状态的转移是确定的而且可以进行直接观测或者间接描述。

（4）功能性验证

功能性验证即验证模型是否满足约束规则。将数据应满足的约束规则通过LTL表达式表示出来，与模型共同作为验证器的输入，若验证通过则说明所建立的模型满足约束条件，若验证不通过则可以给出反例，可定位模型的错误之处并进行修改。由于模型待验证的约束规则过多，因此本文给出以下示例进行介绍。

a.在验证属性域值性质时，如INDEX进程处于indexerror状态则说明该项数据错误，不能直接跳转到进程INDEX，且该状态不能与indexcorrect同时存在。因此需要将该约束条件写成LTL表达式：

notG([indexerror]&[indexcorrect])

b.在数据间有交互作用的验证过程中，比如验证END进程时，首先要保证startpointcorrect和upordowncorrect，才能进行验证，因此需要将该约束条件写成LTL表达式如下：

G([startpointcorrect]&[upordowncorrect])=>F([checkendpoint])

c.在每一个进程检查过程中若出现数据错误，则相应的进程进入ERROR，如检查INDEX2进程中出现index1error则进入ERROR进程，表示数据验证错误。相应的LTL表达式为：

G([index1error])=>F([dataerror])

在ProB检查器中需要通过LTL语句一一验证模型是否满足数据的约束条件，得到的结果正确才能说明该模型正确，部分验证结果如图 3所示。

图  3  LTL语句部分约束规则验证结果

下载: 全尺寸图片 幻灯片

图 3验证结果表明，该模型满足数据的约束规则和无死锁、活锁等要求，本文提出的数据验证流程可用于RDC数据验证。

4   结束语

本文通过对RDC数据进行归纳分析，将实体数据需满足的约束条件总结为属性域值和拓扑关系两方面。以轨道区段数据为例，总结轨道区段数据应满足的约束规则，并对规则进行分类和抽象，再将每个数据字段抽象为独立的进程，将数据约束规则加入验证流程，以终点公里标和索引号数据验证流程为例，利用形式化方法CSP语义对验证流程进行建模，并验证了该模型不存在死锁、活锁，满足确定性的要求，将数据约束条件表示成LTL语句加入验证器，得到验证结果正确，表明该验证流程满足数据约束规则，可用于RDC数据的验证。本文的研究成果确定了RDC数据验证的流程，为下一步RDC数据自动化验证工具的开发奠定了基础。