轨旁资源请求协议的建模与验证
对于轨道交通系统而言，确保有效地管理和解决轨旁资源请求冲突至关重要，以保障其安全、高效的运行。在本文中，我们介绍轨旁资源请求协议建模和验证方法，该协议的主要目标是实现安全资源锁定，这里的安全资源锁定是指没有两个不同的代理同时锁定相同的资源¹，并对该协议进行建模和验证，以形式化的严格方法证明该协议的安全性等相关属性。
案例研究
在图1的轨道网络布局中，列车T1根据运营任务分别向资源管理器1、资源管理器2、资源管理器3和资源管理器4请求区段资源SR1，SR2，SR3和SR4。而列车T0根据其运营任务分别向资源管理器0、资源管理器2和资源管理器3请求区段资源SR0，SR2和SR3。
图1 轨道网络布局
如图2所示，虚线箭头表示需要由代理来锁定的资源。例如，列车T0根据运营任务行驶到SR3，则它必须同时锁定区段SR0，SR2和SR3。
图2 资源锁定
在图3中，我们展示了一个简单的资源锁定协议。每个资源控制器都有一个关联的类似队列的内存，其中可以存储资源分配的顺序。虚线箭头表示需要由代理来锁定的资源，实线箭头表示被代理锁定的资源。资源还有承诺(ppt)指针和锁定(lpt)指针，它们分别表示队列中当前可用的槽位和已被锁定的槽位。
图3 简单的资源锁定协议
通过确保代理锁定的不同资源的槽位值相同，可以预防交叉阻塞类型的死锁。此外，通过代理和资源管理器之间多次的消息确认，可以防止在消息延迟的情况下发生死锁。基于这些考虑，我们定义了一个两阶段通讯协议（如图4所示）。在第一阶段中，规定了代理如何形成分布式通道（即确保锁定的槽位值相同）。而在第二阶段中，解决了在代理形成分布式通道后可能发生的死锁情况²。
图4 两阶段通讯协议
Event-B建模
2.1 模型M0
形式化协议建模是从定义静态模型信息开始的，如载波集、常数和公理³。首先，我们为抽象模型创建一个上下文，其中包含三个有限大小的载波集，分别表示代理(AGT)、资源(RES)和目标(OBJ)。我们还引入了一个枚举集（AST）来表示代理状态。正如前文所述，分布式协议的目标是实现安全的资源锁定，这可以抽象为代理消耗和释放目标（如图5所示）。
图5 模型M0
我们引入了两个变量来存储已消耗的目标（cons）和代理状态（pct0）。
在代理消耗事件中，当一个目标尚未被消耗（grd1）且代理未消耗任何其他目标（grd2）时，更新变量cons，表示代理已消耗该目标。此外，该事件更新了代理的状态，代理由消耗状态变为释放状态，而代理释放事件则相反。
2.2 模型M1
模型M1中，我们引入资源，一个目标可能包括一个或多个资源。代理不是简单地消耗一个目标，而是捕获资源，直到目标完成(如图6所示)。
图6 模型M1
我们引入两个变量来存储代理已捕获的资源（capt）和代理需要完成的目标（objt）。
与仅捕获单一目标不同，一个代理可能需要消耗多个资源来实现其目标。在代理消耗事件b中，代理不断地捕获所需目标的资源（grd2），且该资源尚未被其它代理捕获(grd3)。
一旦代理捕获了目标所需的所有资源，代理可以消费资源并最终释放资源。跟代理消耗事件类似，代理释放事件也被精化。
2.3 模型M2
在这层精化模型中，我们首先引入协议的第二阶段部分。在协议的这个阶段，发送三种类型的消息：代理发送锁定（lock）和释放（release）消息，资源发送（response）响应消息。
在第二阶段中，代理试图通过发送锁定消息来锁定与之相关联的资源。为了对此进行建模，首先是锁定消息发送事件。如果消息lc之前尚未发送且尝试锁定的资源是目标资源，代理会将消息lc加入到锁定消息信道中。此外，代理还会保存已发送的锁定消息。
其次是锁定消息发送完成事件。当代理所需的资源的锁定消息都已发送，该代理会进入确认状态。根据协议，在发送完所有锁定消息后，代理将等待资源的响应消息，然后再继续消耗资源。
为了对响应消息进行建模，首先我们创建了一个读取指针变量rdpt，它作为代理的资源锁。一旦一个资源接收到来自锁定该资源的代理的释放消息，资源锁就会被释放。如果该资源没有被其它代理锁定，回复READY消息，否则，回复DENY消息。
代理必须接收到所有的响应消息才能进行决策。在该模型中，我们创建了代理决策事件,它根据接收的响应消息更新代理的状态为消耗（CONSUME）或者未锁闭（NULOCK）。
2.4 模型M3
在第三次精化中，我们引入了写消息和准备就绪消息，这是将协议阶段一和阶段二连接起来的中间步骤。由于写消息发送事件和准备就绪消息事件与模型M2中锁定消息发送和响应事件类似，我们在这里就不再讨论它们了。
2.5 模型M4
在最终模型M4中，引入了协议阶段一，其中包含了请求（request）消息和回复（reply）消息。由于请求消息的发送事件和回复消息的事件类似于模型M2中的锁定消息发送和响应事件，因此在此不再赘述。
结语
我们未来的研究方向之一是探索协议在实践中部署的可行性。目前轨旁资源请求冲突协议在较高的抽象层次上解决了铁路资源分配问题，在今后的工作中，协议还需要进一步细化，以考虑道岔、信号机、进路等其他铁路信号要素。
- 用户评论