基于时间自动机的列控系统等级转换建模与验证

董家希，刘珂帆，鄢春花，杜利芳，周家宇

（成都工业学院 汽车与交通学院，四川 成都）

引言

在列车运行过程中，需要十分严苛复杂的控制系统对于其安全稳定运行起到保障作用。等级转换作为列控系统中的重要组成部分，每个环节的运作都必须得到严格的检查和确认，方能顺利推进。近年来，对于列控系统进行形式化建模，取得了丰硕的成果。其中，基于时间自动机原理的模型能够将复杂抽象的列控系统等级转换过程更加直观、全面、清晰的呈现出来，因此在实时系统问题的研究中具备良好的表现[1]。

1 时间自动机模型

1.1 时间自动机理论

时间自动机(Timed Automata, TA)是一种面向实时系统进行建模和验证分析的理论，为具有时间特征的系统的状态转换图的描述提供了一种简洁有效的方法[2]。

时间自动机系统将复杂的实时系统抽象为状态和边的转换关系，并为其转移条件提供了相应的时钟约束，每个状态改变都可以配合触发启动对应的时钟计时模式，这个时钟约束所对应的转移条件在满足时钟约束的条件下才能够执行。

时间约束的集合(X)的定义如下：

其中，X 表示时钟变量，x 表示其中一个时钟，时钟解释表示为时钟集X 上的每一个时钟赋予的一个实数值。

其中，T⊆R+，Tx为X 上所有时钟解释的集合。

在一个复杂的实时系统中，常常是由多个子系统构成的，他们之间相互独立又彼此配合，频繁进行子系统之间的信息交互，保证整个系统的协同合作，从而完成复杂实时系统对应的功能。因此我们可以用组成该系统的各个子系统的积来描述系统的功能，称为时间自动机的积[3]。

设两个时间自动机TA1=，TA2=，时钟集合X1和X2不相交，则TA1和TA2的积记为TA1|| TA2。

1.2 UPPAAL 建模

UPPAAL 软件采用图形化的界面，主要由四个部分组成[4]。System Editor 是用于创建实时系统建模的工具。Simulator 是建模的初始步骤，它以图形方式表示系统的逻辑关系。Verifier 则是实现系统功能仿真和时序仿真的关键工具。在设计阶段Verifier 可以检查所有可能的执行路径，并在验证之前对已有模型进行检验。Yggdrasil则用于测试用例的自动生成，可进行深度搜索，分析其测试用例覆盖的运营场景，还可以根据所验证性质进行测试用例的自动生成。UPPAAL 结构体系见图1。

图1 UPPAAL结构体系

TA 模型包括状态、边和约束条件三个元素。在TA模型中，两个子系统之间的信息交互通过通道完成。UPPAAL 中所支持的BNF 语法主要有4 种表现方式[5]，其BNF 语句及含义见表1。

表1 BNF 语句及含义

2 等级转换场景需求分析

2.1 等级转换场景过程分析

当列车进行C2 到C3 等级转换时，边界上设置了应答器、转换点以及司机确认区等，具体布置见图2。

图2 等级转换边界布置示意

2.2 建立等级转换信息交互图

将C2 至C3 列控系统等级转换流程场景抽象描述为司机、应答器、车载设备和RBC 四个子系统之间的信息交互过程。它们通过传输包含不同指令的信息包来进行信息的传递。

对于根据需求规范归纳出来的C2 至C3 列控系统等级转换流程的描述，绘制了C2 至C3 级列控系统等级转换流程信息交互序列图见图3。

图3 等级转换流程信息交互序列图

3 等级转换场景建模与验证

在构建模型时，我们将整个系统划分为Train、Balise、RBC 和Driver 四个子系统，并分别构建这些子系统的UPPAAL 模型。

3.1 等级转换场景建模

在等级转换场景建模中，车载子系统是其中最复杂的部分。当列车通过等级转换区域时，车载子系统根据列车实时状态，频繁地与应答器、RBC 以及司机界面进行信息传递，以确保等级转换顺利进行。等级转换Train子系统模型见图4。

应答器子系统作为车地信息交互的渠道，用于判断列车位置，根据需求不同设置的相应功能的应答器，可以实现列车定位，为等级转换提供位置信息。等级转换Balise 子系统模型见图5。

图5 等级转换Balise 子系统模型

RBC 根据收到信息生成控制命令，提供行车许可，保证列车运行安全性，模型见图6。

图6 等级转换RBC 子系统模型

当接收到RBC 传送的等级转换命令后，车载设备就会向司机发送等级转换确认请求，司机通过按压按钮对于等级转换过程进行确认。这样可以通过自动化操作和人工操作两个方面来完整地验证列控系统等级转换的条件，实现双保险。等级转换Driver 子系统模型见图7。

图7 等级转换Driver 子系统模型

3.2 等级转换场景模型验证

得到状态转移图后，还需要运用UPPAAL 的验证器对模型进行进一步的验证，保证模型的正确性。利用形式化验证的方法确保模型满足系统的功能性需求和实时性需求，其流程见图8。

图8 基于UPPAAL的形式化验证流程

功能性要求主要关注研究所建立的模型对于转换流程的完整性。例如，确保系统能够按照实际流程顺利完成所需的步骤，防止系统出现死锁，并确保执行操作能够正常进行。同时，在设备正常运行的情况下，系统应能够实现从C2 级到C3 级列控系统的等级转换。当转换条件不满足时，系统应能够保持C2 级列控系统的控车运行等。等级转换功能性要求验证运行结果见图9。

图9 等级转换功能性要求验证结果

实时性要求主要验证系统的时间特性。等级转换场景对时间的要求十分严格，因此，模型中状态迁移的时间约束能否有效合理进行是模型建立成功与否的关键因素。等级转换实时性要求验证运行结果见图10。

图10 等级转换实时性要求验证结果

经过等级转换过程中对每条性质的逐一验证，得出的验证结果发现每条性质均是可达的，说明系统可以满足相应的性能和需求，证明所建立的时间自动机模型是安全可靠的。

4 结论

本文提出了一种基于模型对于复杂实时系统的研究方法，并对模型的准确性及完备性进行形式化验证。首先，对于列控系统的等级转换场景进行过程性分析和提取需求，梳理各子系统之间的信息交互流程。其次，基于时间自动机原理，借助UPPAAL 建模工具，建立四个子系统的状态转移图模型。最后，对标列控系统规范要求，结合BNF 逻辑公式和系统验证器，对于模型的实时性和功能性需求给出验证，保证了此模型的准确性和可靠性。对于基于模型的研究问题具有一定的借鉴意义。