应答器报文编制规则的形式化建模与验证

黄 旭，刘中田

(1. 中铁第一勘察设计院集团有限公司， 陕西西安 710043; 2. 北京交通大学电子信息工程学院，北京 100044)

应答器作为列车控制系统中必不可少的设备，其向车载设备传输的报文数据是生成控车曲线的依据。CTCS-2级应答器报文直接用于ATP控车，应答器报文编制错误可能导致列车超速或冒进，严重影响列车运行安全。当前应答器报文生成过程为：“列控数据-用户报文-传输报文”。从列控数据到用户报文的过程通常是基于《CTCS-2级列控系统应答器应用原则》[1](以下简称应答器应用原则)和《列控数据管理暂行办法》[2]直接编写软件经人工操作来完成，用户报文到传输报文的编码依据是行业规范SUBSET-036[3]。应答器应用原则是编制应答器报文的标准规范，报文数据的正确性与应用原则的正确性及其被正确理解和应用息息相关，但应用原则存在两个问题：(1)应答器应用原则只规定应答器的设置原则和报文的结构等内容，没有描述具体的编制报文规则，完备性不足。(2)基于文本语言描述的应答器应用原则易产生二义性问题，存在较大隐患。针对这两个问题，需要对应答器应用原则分析整理，得到明确的报文编制规则以解决完备性问题；对于文本语言描述产生二义性的问题，可采用形式化方法来描述应用原则，使得应用原则以唯一的方式被解释，可以有效排除自然语言的二义性，且形式化的描述为进一步形式化分析和验证提供了可能性，这对确保应答器报文正确性有重要意义。

对于列控数据的安全性，文献[4]对各类列控数据间的约束关系进行了深入研究，提取了验证列控数据的逻辑规则，并证明了所提取规则的可满足性，对确保列控数据的正确性有重要的作用。文献[5-6]对用户报文到传输报文的编码过程及方法进行深入研究，使得这一环节的安全性有所保障。而“列控数据-用户报文”这一环节缺乏严格和深入的理论研究。目前国内外对应答器报文编制规则的研究较少，相关研究有从工程实施角度对应答器应用原则部分内容进行分析，对报文发送原则提出优化措施[7]，还有针对应答器布置阶段，用数学语言对应答器应用方案进行描述，并结合应答器应用原则提出一套应答器应用方案的验证和优化方法[8]。已有的研究均是在已有应答器应用原则的基础上对其从经济和工程的方面进行优化改进，但均未从安全的视角对应答器应用原则进行研究。

列控系统是典型的复杂安全苛求系统，根据国际标准IEC 61508，对于高安全系统推荐使用形式化方法进行分析[9]，针对上述应答器报文编制过程存在的问题，本文深度分析应答器应用原则中规定的各信息包之间的关联关系，结合列控数据的格式，提取得到应答器报文的编制规则。对于提取所得的应答器报文编制规则，采用UML与NuSMV相结合的方法进行形式化建模与验证，分析验证结果，得到应答器应用原则存在的问题，并经过反例追踪、定位、修改和重新验证应用原则，可以得到报文编制规则的UML模型，有效避免了文本语言存在的二义性问题，这对提高报文的正确性有着积极的作用，也对保障列控系统的安全运行具有重要意义。

1 应答器报文编制规则的提取

CTCS-2级列控系统应答器应用原则中[1]描述了应答器报文结构、用户信息包变量的含义和不同用途应答器所应包含的报文内容，但并未具体描述如何从列控数据中获取得到报文，且应答器应用原则中存在较多模糊的描述，如5.3.11节中定位(DW)应答器报文编制规则中ETCS-72包的数据范围描述为“车站名称提前三个闭塞分区显示，列车越过出站口后停止显示”，没有具体说明数据起点和终点，只能凭借人工摸索。

列控数据主要由应答器位置表、信号数据表、坡度表、速度表、分相信息表、线路断链明细表、车站信息表等组成，分别对应应答器报文中不同的用户信息包。本文根据应答器报文中各用户信息包之间的关联关系，结合列控数据的内容及格式，整理出应答器报文编制规则，规则的整理思路如图1所示。

图1 应答器报文编制规则的整理方法

将整理得到的规则总结为两部分：一是确定用户信息包种类，二是生成信息包内容。以区间无源应答器报文生成场景为例，表1为提取得到的报文编制规则示例。

2 基于UML-NuSMV形式化建模与验证方法

UML(Unified Model Language)是一种统一建模语言，是对面向对象开发系统的产品进行说明、可视化和编制文档的一种标准语言。UML直观易懂的特点使其被广泛应用于各个行业。但其图形化的符号缺乏精确的语义，并且缺乏分析验证工具的支持[10]。

对比之下，形式化方法是以数学为基础，用数学的方法来解决工程领域的问题，其目标是对系统建立精确的数学模型并对模型进行分析，在工业安全系统中已得到广泛认可[11]。模型检验是一种自动验证有穷状态系统是否具有所期望的性质的形式化方法[12-13]，其对应的数学模型是有穷状态系统；使用时态逻辑语言对期望的系统性质进行描述；自动验证的方法是遍历有穷状态系统的每一个状态，最终给出系统模型是否具有期望性质的结论[13]。NuSMV (New Symbolic Model Verifier)是新型的符号模型检验工具，用以检测一个有穷系统是否满足指定的性质，支持计算树逻辑和线性时序逻辑描述系统性质，若不满足则给出反例，用于回溯定位验证结果。

表1 应答器报文编制规则示例

本文对应答器报文编制规则建模的验证使用UML与NuSMV相结合的方法，如图2所示。

(1)规则管理阶段

对提取所得的应答器报文编制规则进行管理，确保后续模型与规则的一致性和覆盖性。

(2)建模阶段

基于特定场景建立应答器报文编制规则UML模型，并对UML模型进行扩展与抽象，随后将规则的UML模型转换为NuSMV语言模型；基于规则管理的结果，用时序逻辑来刻画编制规则应满足的性质，将两部分输入作为模型检验工具。

(3)模型验证阶段

模型检验工具NuSMV遍历搜索输入的有穷状态系统模型，检验系统模型是否满足指定的性质。

(4)模型检验结果分析

若系统不满足指定的性质，则根据反例验证结果对错误进行回溯、定位、修改和重新验证。

2.1 面向NuSMV的UML建模

基于整理后的报文编制规则，建立编制规则的UML类图、状态转移图。UML类图是用类及其相互关系对系统进行静态描述。UML状态图是对系统动态行为建模，描述对象的不同状态之间转换的条件和响应。报文编制规则对应的UML模型中包含大量与验证系统特性无关的数据，如果用NuSMV直接遍历这些数据，会大幅增大系统的状态空间，甚至会引发状态爆炸。因此为了确保系统模型的可验证性和验证过程的高效性，需对报文编制规则的UML模型进行扩展和抽象。

(1)面向NuSMV的UML模型扩展

事件是一种允许系统对象和外界交互的消息机制，本文结合NuSMV的特性，在UML的基础上引入输入输出事件，用布尔型数据代替字符型或整型数据。如报文编制规则中的应答器组位置，编制规则需要得到的是该应答器组的位置是否在分相区范围内，而应答器组的坐标取值对于模型检验而言无任何意义，因此可引入“应答器在分相区内(Balise in_DZ)”事件，取值为1时表示本应答器处在分相区范围内，取值为0则代表不在。

(2)面向NuSMV的UML模型抽象

完整的报文编制规则UML类图中会存在大量与待检验系统性质无关的特性和操作，抽象是一个缓解状态问题最有效的方法之一，因此需要对原模型进行抽象，保留与待验证性质相关的变量即可。此过程应根据影响锥COI(Cone of Influence)分析[14]，以确保抽象后的模型性质能与原模型保持一致。

2.2 NuSMV建模

将2.1节中扩展和抽象后的UML模型转换为NuSMV模型，转换规则如下：

(1)NuSMV系统结构

NuSMV程序语言由若干模块(MODULE)组成，主要包括一个Main模块和若干子模块。其中Main模块描述整个系统的组成以及待验证的系统性质，待验证的系统性质用SPEC关键字进行声明，子模块与UML中每个类意义对应。

(2)MODULE部分

UML模型中每个类的输入事件对应相应MODULE的形式化参数，并且在每个输入事件前加前缀“in_”作为模块输入参数名，作用是使子模块与主模块关联。

(3)VAR部分

变量声明使用关键字VAR，主要用来创建组件关系、声明模块状态机状态和类的属性。每个类的属性转换为对应MODULE的VAR下的变量；每个属性的数据类型转换为对应变量的数据类型；状态机的状态应在VAR部分声明。

(4)ASSIGN部分

变量赋值使用AGGGN关键字，主要用来说明状态和属性的初始变化以及变化机制。

具体NuSMV语言可以参考NuSMV指南和用户手册。

2.3 NuSMV模型检验及结果分析

2.3.1 模型检验

NuSMV模型检验使用特定的遍历搜索算法来检验系统模型是否满足指定的性质，算法详见文献[15]。模型检验的基础是将系统应满足的性质用CTL(Computation Tree Logic)公式描述。 CTL由路径谓词和时态运算符两部分构成：路径谓词有两类，分别是A(对所有路径)和E(存在一个路径)；时态运算符主要包括G,F,X,U， G(Goble)指所有状态、F(Future)指未来的某个状态、X(neXt)指下一个状态、U(Until)指直到某一状态。将系统性质和系统模型输入模型检验工具NuSMV进行模型检验。

(1)活性验证

系统的活性是指从任何状态系统都可以达到状态s1。对应验证的CTL公式为：AG(EF(state=s1))。

(2)转移性验证

转移性是指系统在状态s1和状态s2间可以互相转移。对应验证的CTL公式为：EF(state=s1 & EX(state=s2))。

(3)反应性验证

说明R出现的条件，即表明S和R的因果关系；如果S出现，则R终将出现。验证反应性的CTL公式为：AG(S -> AF(R))。

CTL算子“->”关系真值表见表2。

(4)互斥性

互斥性是指系统的某两个状态一定不会同时出现。对应验证的CTL公式为：!EF(state=s1 & state=s2)。

(5)确定性验证

表示系统不会同时处于状态s1和状态s2。与互斥性类似，但不同的是确定性对应的是系统的无线运行状态。验证确定性的CTL公式为： !AG(state=s1 <-> state= s2)。

2.3.2 反例分析

对验证结果进行分析，如果系统不满足验证性质，NuSMV会给出反例来解释逻辑公式不成立的原因。反例分析的方法是：按照反例提示，逐步检查NuSMV系统建模、模型抽象、UML建模过程是否存在错误。如以上都无误，最后确认所提取的报文编制规则是否存在问题或是应用原则存在问题。如此逐步回溯定位，直至检验结果全部为TRUE或着找到应用原则的问题。

3 报文编制规则的UML建模

针对报文编制规则的管理结果，本文以Q应答器报文的生成场景为例，建立应答器报文编制规则的UML类图、时序图和状态图。

3.1 UML类图

采用面向对象的方法将编制规则抽象为4个相互关联的类，分别是信息包种类确定器类InfoTypeConfirmer、信息包内容生成器类InfoContentCreater、列控数据类EngDataTables和用户报文类UserDataPackets，其中信息包内容生成器类包含了Head、E5、C1…等生成子类。图3所示为扩展和抽象后的UML类图，每个类都有其对应的接收信息和输出操作，接收信息以≪signal≫开头，输出操作以“+”开头。例如InfoTypeConfirmer的接收信息有BaliseInfo()，输出的操作是Con_E5()、Con_C1()等，具体字段含义见表3。

图3 报文编制规则的UML类图

名称含义BaliseInfo()本应答器组信息(位置,公里标,用途,类型,编号)N&S_BaliseInfo()下一组和第二组应答器信息Last_BaliseInfo()上一组应答器信息SecondQ()本应答器前方第二个Q应答器组公里标PosSignal_FJZFJZ信号机的公里标NextQ_FJZ本应答器组前方的FJZ信号机外方第一个Q应答器组信息DataScope()轨道区段数据范围GradientInfo()数据范围内的坡度信息SpeedInfo()数据范围内的速度信息Con_E5(),Con_C1(),…确定包含E5、C1、…信息包Create_E5(),Create_C1(),…生成E5、C1、…信息包E5_Created(),C1_Created(),…E5、C1、…信息包已生成Find_Q_JZ()寻找JZ外方第一个和第二个Q应答器组信息Find_DataScope1/2()寻找数据范围(是/非JZ外方应答器)TP1(2)()数据打靶点(是/非JZ外方应答器)DZ_Info()分相区信息BD()列车的最大制动距离C1_LPACKERC1信息包位数

3.2 UML状态转移图

状态图主要用来描述对象、子系统、系统的生命周期，模型检验的理论基础是有穷状态系统，状态图是后续模型检验中有限状态机的基础。构建区间应答器报文编制规则的UML状态图，如图4所示。

图4 报文编制规则的UML状态转移图

其中列控数据类包含信号数据子类、应答器位置表子类等；信息包内容生成器类包含各类具体的信息包生成器子类。特性和事件的含义见表3。

4 报文编制规则的NuSMV建模与验证

4.1 NuSMV模型

依照前文的方法，将扩展和抽象后的UML系统模型转换为NuSMV模型，UML模型中每一个类对应NuSMV模型的一个MODULE。以Q应答器生成场景为例，以下为Main模块和C1信息包内容生成模块对应的NuSMV模型片段截取。

Main模块片段与C1信息包内容生成模块：

MODULE main()

VAR // 声明变量

BaliseInfo: boolean;

infoContentCreater: InfoContentCreater(…);

engDataTables: EngDataTables(…);

userDataPackets: UserDataPackets(…);

infoTypeConfirmer: InfoTypeConfirmer(…);

state: {Idle,BaliseTele_Created};

ASSIGN

init(BaliseInfo) := 0;

init(state):=Idle; // 定义初始状态

next(state):= // 状态转移

case

state = Idle &(userDataPackets.UDP_Created=1): BaliseTele_Created;

TRUE : state;

esac;

SPEC AG (BaliseInfo=1 -> EF state_BaliseTele_Created) //待验证的规范

⋮

C1信息包内容生成模块：

MODULE Info_C1(in_Con_C1, in_DataScope, in_Balise_is_Q_JZ, in_C1_LPACKET, in_E44_Created)

VAR

out_Create_C1: boolean;

out_Find_Q_JZ: boolean;

out_Create_E44: boolean;

⋮

state: {Idle, C1_Confirmed, Find_DataScope, DataScope_Confirmed, E44_Confirmed, C1_Created};

ASSIGN

init(out_Create_C1):= 0;

init(out_Find_Q_JZ):= 0;

init(out_Create_E44):= 0;

init(state):= Idle;

⋮

next(state):=

case

state = Idle & in_Con_C1=1 : C1_Confirmed;

state = C1_Confirmed & in_Balise_is_Q_JZ=1: Find_DataScope;

state = C1_Confirmed & in_Balise_is_Q_JZ=0: Find_DataScope;

state = Find_DataScope & in_DataScope=1: DataScope_Confirmed;

state = DataScope_Confirmed & in_C1_LPACKET=1: E44_Confirmed;

state = E44_Confirmed & in_E44_Created=1: C1_Created;

TRUE : state;

esac;

⋮

4.2 NuSMV模型的检验及结果分析

4.2.1 模型检验

对报文编制规则的NuSMV模型进行检验，由于模型待检验特性过多，因此本文仅对检验过程进行举例介绍。

(1)活性验证

例如表达式SPEC AG(EF(infoTypeConfirmer.state=InfoType_Confirmed))表示从任何状态，经过某些步骤可以确定用户信息包种类。验证结果为true。

(2)转移性验证

例如SPEC AG (state=Idle & EX(state= BaliseTele_Created))，表示报文编制结果能够从状态为空一步转移到报文已生成状态。验证结果为true。

(3)反应性验证

例如表达式SPEC AG (infoContentCreater.info_C1.state= C1_Confirmed -> AF infoContentCreater.info_C1.out_Create_E44=1)的含义是：如果确定改组应答器报文中含有C1包，则E44包一定已生成。验证结果为true。

(4)互斥性

例如表达式SPEC !EF(infoContentCreater.in_BD=0 & infoContentCreater.info_C1.state= C1_Created)，表示找不到制动距离，则无法生成C1信息包。验证结果为true。

(5)确定性验证

例如表达SPEC !AG(infoTypeConfirmer.out_Con_E5=0 <-> infoContentCreater.info_E5.state= E5_Created)，表示确定没有E5包和E5包的内容已生成的两个状态一定不可以同时出现。验证结果为true。

4.2.2 结果分析

如果某些系统性质的验证结果不是true，而是false，则需要根据NuSMV给出的反例对错误进行回溯追踪、定位和修改，重新验证修改后的模型。以下是由于文本语言描述应答器应用原则存在二义性导致在建模过程产生的反例，以此来说明反例结果分析的过程。

在深入分析挖掘应答器应用原则中描述的各信息包的内容可以得出：区间应答器报文应满足“如该区间应答器组报文中生成了C1包，则该组报文一定已生成E44(C1)包”的特性。针对本条特性的模型检验的结果最初为false,验证结果中反例提示为“没有找到E44(C1)包已生成的状态”。因此需对该反例进行分析，首先检查系统NuSMV程序，确认没有逻辑错误，符合UML模型的描述；再反向检查UML模型，与区间应答器组报文编制规则一致；再继续追溯，发现在应答器应用原则中并未提及[ETCS-44]与CTCS包应有的关系。最终错误定位在对于《CTCS-2级列控系统应答器应用原则》5.2.6.1节 “每个[ETCS-44]包只能嵌入一个CTCS包”[1]这句规则的理解，应在应用原则中补充“每个CTCS包必须嵌入[ETCS-44]包才可作为完整的用户信息包存在”，防止误解。

4.2.3 模型检验的结论

对报文编制规则的NuSMV模型进行全面验证，验证结果均为true，表明所提取的应答器报文编制规则满足活性、转移性、无死锁性、确定性等要求。同时根据反例分析过程可以得到应答器应用原则存在的问题，即文本语言描述存在二义性。

5 结论

本文论述了应答器报文数据以及其编制规则的重要性，指出《CTCS-2级列控系统应答器应用原则》[1]描述模糊，用文本语言描述存在二义性等问题，深度分析报文数据之间的关联关系以及报文与列控数据之间的关联关系，总结得到编制规则；采用UML与NuSMV相结合的方法对应答器报文编制规则进行形式化建模与验证，验证了编制规则的转移性、活性、反应性等，最后在反例分析的过程中可以发现应答器应用原则存在的问题。验证过程表明：

(1)UML与符号模型检验相结合的方法适用于应答器报文编制规则的验证。

(2)基于UML与符号模型检验相结合的形式化方法，能够识别基于文本语言描述的应答器应用原则存在的二义性。

(3)通过对模型验证的反例分析，可以建立正确且被唯一理解的应用原则UML模型，用UML描述的应用原则在实际应用中可避免二义性问题，对于提高应答器报文数据生成过程的正确性有重要意义。