基于扩展标记变迁模型的时钟同步协议正确性验证

曲国远，徐晓飞，刘威廷，王沁煜，贺 飞

(1. 中国航空无线电电子研究所， 上海 200233； 2. 清华大学 软件学院， 北京 100084；3. 北京信息科学与技术国家研究中心， 北京 100084； 4. 信息系统安全教育部重点实验室， 北京 100084)

时间触发网络[1-3]被广泛应用于航空航天、轨道交通、军事装备等实时性要求高的系统中。在时间触发网络中，所有网络消息都由预先定义的时刻进行触发。时间触发网络能够保证网络中每一个终端在某一个时刻最多只能发送一条消息。相比于传统的基于事件触发的网络，时间触发网络具有更好的通信实时性和确定性。

时间触发网络必须实现网络中所有设备的时钟同步。考虑每一个网络设备都有自己的本地时钟，不同设备的本地时钟之间存在偏移，并且这个偏移在经过一定时间的累积后，可达到一个不可忽视的程度。时间触发网络利用时钟同步协议建立一个全局统一的系统时钟，并且基于该系统时钟调度网络中的所有通信。

时间触发网络在我国航空航天、轨道交通等领域有很好的应用前景。在将该网络引入这些应用领域前，需要进行适应性的补充与修改。如何证明修改后的时钟同步协议仍然具有正确性成为制约时间触发网络在这些系统中进行应用的关键。

本文以扩展标记变迁模型描述协议行为，以时序逻辑刻画正确性属性，基于模型检测工具Beagle[4]，对协议是否满足属性进行形式化验证。

1 扩展标记变迁模型

模型检测[5-6]是一种用于有限状态并发系统的形式化验证技术，在电路验证、通信协议验证、软件验证中已经取得了巨大的成功。给定系统M和正确性属性P，模型检测通过搜索M的所有状态(或者所有执行路径)来判定M是否满足P。

在给定网络节点的情况下，时间触发网络[1]就是一个典型的有限状态并发系统。标记变迁(Labeled Transition System, LTS)模型是一种经典的、针对有限状态并发系统的形式化模型。

定义1(LTS模型)令AP为原子命题集合，一个标记变迁模型是一个四元组M=(Σ,S,S0,R),其中Σ是标记的有限集，S是状态的有限集，S0⊆S为初始状态的集合，R∈S×Σ×S是变迁关系。

设s,t∈S为系统的两个状态，α∈Σ为系统的一个标记，如果〈s,α,t〉∈R，则称之为系统的一条变迁。设r∈R为系统M的一条变迁，以l(r)表示r上对应的标记。

标记变迁模型中S为系统中所有状态的集合。当系统状态空间较大时，难以直接使用LTS进行建模。扩展标记变迁(Extended Labeled Transition System, ELTS)模型在LTS的基础上扩展了变量，能够更方便地描述规模较大的系统。

定义2(ELTS模型)令AP为原子命题集合，一个扩展标记变迁模型是一个七元组M=(Σ,X,S,S0,R,τ,η),其中(Σ,S,S0,R)是一个LTS模型；X是变量的有限集；τ为每条变迁r∈R定义了一个被称为守护条件的表达式g(r)；η为每条变迁r∈R定义了一个对X中变量进行赋值的动作序列a(r)。

ELTS模型的状态是对X∪L的一组赋值，称ELTS中的L为控制状态集合。设r∈R为系统的一条变迁，r常被表示为：

l(r)[g(r)]:a(r)

图1给出了一个信号灯控制系统的ELTS模型。该模型中含有2个控制状态，即Red和Green，分别代表红色和绿色信号灯。模型中含有1个变量x，代表时间。为简单起见，图中守护条件为true时可以省略，动作序列为空时也可以省略。该信号灯控制系统的初始控制状态为Red，从Red到Green的边

t3[x=15]/x++

表示该变迁在x的值等于15时可以被触发，并且执行该变迁会导致x的值加1。其他边可以类似地进行分析。

定义3(简单安全属性验证)给定一个模型M和一条属性P，如果在M的所有状态上P都成立，则称M满足P(记作MP)。

以图1为例，假设属性为x<60，显然该属性在M的所有状态上都成立，所以MP成立。

图1 ELTS示例图Fig.1 An ELTS example

2 时钟同步协议

时间触发网络[1]按照事先设定的时刻来协调网络中的数据交换。在时间触发网络中，不同网络终端的本地时钟之间存在偏移，并且这个偏移会随着时间累积。为实现时间触发网络，必须借助时钟同步协议，将网络中所有设备的时钟误差控制在一定范围内。

时间触发网络[1]中的设备主要包括交换机和终端。在时间触发网络中，一般称终端设备为同步主(Synchronize Master, SM)，交换机为压缩主(Compression Master, CM)。图2给出了一个包括4个同步主和1个压缩主的时间触发网络，其中实线代表设备之间的物理连接。

图2 时间触发网络示意图Fig.2 The time-triggered network

时钟同步协议的主要过程是CM收集SM的本地时钟，计算全局时钟，然后再分发给SM的过程。CM和SM之间的数据交换主要依赖协议控制帧(Protocol Control Frame, PCF)进行。处于空闲状态的CM接收到SM的PCF后，进入收集状态。处于收集状态的CM开启一个时间窗口，并在该时间窗口内等待后续PCF。如果CM在时间窗口内接收到一个新的PCF，将向后延长一个窗口长度的等待时间。当CM收集到的PCF数量达到阈值或在一个窗口时间内没有收集到任何新的PCF，CM进入到计算状态。在计算状态下，CM对收集到的所有时钟进行计算，并将计算结果分发给所有SM，供SM进行时钟同步。

时间触发网络支持双CM备份。一个包含2个CM的时间触发网如图3所示。在双CM备份网络中，为防止主CM故障导致网络结构瘫痪，设置备用CM用于故障恢复。所有SM会同时向两个CM发送PCF，两个CM独立地运行同步协议，将分别计算全局时钟并发送给所有SM。SM在收到来自两个CM的全局时钟时，有多种策略，例如只采用主CM的时钟、采用两个CM时钟的平均值等。本文假定SM采用前一个策略，即只使用主CM时钟。

图3 双CM冗余时间触发网络Fig.3 A time-triggered network with double CMs

将时钟同步协议应用到航空航天等实际系统中时，系统启动是相对容易出错的时刻。本文讨论了多种启动模式下时钟同步协议的正确性。

1)单CM启动模式：在普通启动模式下，系统中仅含一台交换机(即CM)。这种启动方式比较简单。在初始条件下，CM上电后处于非同步状态。主管理器正常启动后启动PCF发送，CM收到PCF后进入同步状态，并转发PCF。各个SM上网后，同步到CM转发的PCF时间，周期性地发送PCF，参与时间同步过程。

2)双CM同步启动模式：在该模式下，系统中包含两台CM，并且两台CM同步启动。首先双CM上电后处于非同步状态，主管理器争权成功，通过双通道启动PCF发送，两个CM收到PCF后，都进入同步状态，并转发PCF。各个SM上网后，从工作网络接收PCF，并同步时钟，周期性地通过双通道发送PCF，参与时间同步过程。

3)双CM异步启动模式：双CM异步启动的工作模式允许先在单CM的情况下工作一段时间后再将另一个CM加入时间同步网络。与同步启动模式相比，异步启动更灵活且适用性更广。首先，单CM上电，系统进入时间同步状态。另一个CM上电，进入非同步状态。各个SM节点通过双通道发送PCF给双CM，CM进入同步状态，并同步到接收的时钟，用第一个接收到的时钟设置本地时钟，可以和接收到几个时钟无关。各个SM周期性地发送PCF参与同步，各个SM依旧同步到工作网络。

3 协议建模

基于扩展标记变迁模型[4]对时钟同步协议进行建模，所建模型主要包含4个模块，分别是压缩主CM模块、同步主SM模块、触发器TRIGGER模块和监视器MONITOR模块。

3.1 CM模块

CM模块包含五个控制状态，分别为：初始状态START、空闲状态IDLE、收集状态COLLECTION、延迟状态DELAY和计算状态CALC。CM模块的ELTS模型如图4所示。为方便阅读和理解，在图4中只标出了每条迁移边对应的同步标记，守护条件和动作序列都被隐去。

图4 CM模型示意图Fig.4 The CM model

处于START状态的CM接收到start同步标签后进入IDLE状态，此时CM会等待SM发送PCF。当收到第一个PCF后，CM进入COLLECTION状态。处于COLLECTION的CM循环等待不同的SM发来的PCF，直到收到的PCF数量等于所有SM的数量。之后CM进入DELAY状态，延迟一段时间并通过时间同步算法计算出统一时钟，然后进入CALC状态，通过calc同步标签对各个SM进行时间同步。最后在转移回START状态之前，CM通过agree_sync同步标签通知MONITOR模块已经完成时间同步，从而模拟分发统一时间的PCF，等待下一个循环周期的开始。

下面定义图4中每一条迁移边的守护条件和动作序列。首先引入下列变量：

int clock;

int current_reading_index;

int SM_amount;

int delay_timeout;

其中，clock是CM的本地时钟，current_reading_index是CM当前收到的PCF数量，SM_amount是系统中SM数量，delay_timeout代表了CM计算统一时间时需要延迟的时间长度。

假设r是模型中从控制状态s0到s1的一条迁移边，l(r),g(r)和a(r)分别表示r的标记、守护条件和动作序列。本文使用下面的文法表示r:

froms0tos1onl(r) providedg(r) doa(r);

根据上面的文法，CM模块从START状态到IDLE状态的变迁可以表示为：

from START to IDLE on start do {

clock = 0;

SM_amount = 5;

current_reading_index = 0;

delay_timeout = 5;

};

这条变迁的守护条件为true，执行该变迁将对CM中的各个变量进行初始化操作。

CM模块从IDLE状态到COLLECTION状态的变迁表示为：

from IDLE to COLLECTION on dispatchi

provided (current_reading_index == 0)

do {

current_reading_index = 1;

};

该变迁必须在current_reading_index==0的条件下由第i个SM发出的dispatchi触发，执行该变迁将赋值current_reading_index=1。

CM模块从COLLECTION状态到COLLECTION状态的变迁表示为：

from COLLECTION to COLLECTION

on dispatchi

provided

current_reading_index < SM_amount

do {

current_reading_index =

current_reading_index + 1;

};

这是CM收集不同SM发出的dispatchi时执行的变迁，该变迁反复执行，直到CM收到的PCF数量等于系统中SM的总数，每次执行导致current_reading_index的计数加1。

DELAY状态模拟了CM收集完所有SM发来的本地时钟后进行全局时钟计算所产生的延迟。这里的 delay_timeout为预先设定的一个延迟时间。CM模块从COLLECTION状态到DELAY状态，从DELAY状态到CALC状态的变迁的守护条件均为true，动作序列都为空，其文法表示省略。模型中定义这两条变迁的目的主要是为了与其他模块同步。

CM模块从CALC状态到START状态的变迁表示为：

from CALC to START on agree_sync

provided delay_timeout == 0 do {

current_reading_index = 0;

delay_timeout = 0;

clock = clock + 1;

};

该变迁主要用于各个变量值的重置，以及利用agree_sync标签与MONOITOR模块同步，表示CM的一个计算周期结束。

3.2 SM模块

SM模块的行为与网络中包含的CM个数相关。下面分情况讨论单CM网络和双CM网络中SM模块的形式化模型。

3.2.1 单CM网络的SM模块

单CM的SM模型包含四个控制状态，分别是：初始状态START、空闲状态IDLE、分发状态DISPATCH和同步状态SYNC。其ELTS模型如图5所示。同样，在图5中只标出了每条迁移边对应的同步标记，隐去了守护条件和动作序列。

图5 单CM的SM模型Fig.5 SM model in a single-CM network

处于START状态的SM模块收到start标签后进入IDLE状态。当SM的本地时钟到达预定的发送时刻，SM会发送一个PCF给CM，然后进入DISPATCH状态。SM在进入DIAPATCH状态后会等待，直到CM计算出全局时钟。最后，SM收到CM计算的全局时钟，进入SYNC状态完成时钟同步。

为详细定义SM模块的每条迁移，需要引入下列变量：

int clock;

int dispatch_timeout;

int deviation;

其中，clock是SM的本地时钟，dispatch_timeout是预先设定的发送时间点，deviation则是为了模拟现实的晶振误差和传输延迟所设定的一个时间偏移。模型中会设定deviation为一个0到5范围内的随机数。

SM模块从START状态到IDLE状态的变迁表示为：

from START to IDLE on start do {

clock = dispatch_timeout + deviation;

dispatch_timeout = 0;

deviation = 0;

};

这个迁移由start标签触发，会将SM的本地时钟置成dispatch_timeout与deviation的和，表示CM收到的SM的本地时钟存在时间偏移。

SM模块从IDLE状态转移到DISPATCH状态的变迁表示为：

from IDLE to DISPATCH on dispatchiprovided

deviation ==0 && dispatch_timeout == 0;

该迁移需要满足deviation和dispatch_timeout的值都为零的守护条件才能触发，执行此迁移将发送第i个SM的dispatchi标签给CM模块。

SM模块从DISPATCH状态到SYNC状态的变迁表示为：

from DISPATCH to SYNC on calc do {

clock = CM.clock;

};

当处于DISPATCH状态的SM收到CM模块发出的calc标签时，表示CM已经完成了时间同步，此时需要将SM的本地时钟更新成CM的全局时钟，并转移至SYNC状态。

SM模块从SYNC状态到START状态的变迁表示为：

from SYNC to START on sync;

当SM处于SYNC状态时代表了SM的本地时钟已经处于了同步状态，需要等待所有其他SM都到达同步状态后一起返回START状态完成一个同步周期。

3.2.2 双CM网络的SM模块

双CM网络中SM模块的ELTS模型如图6所示。相比于单CM网络的模型，该SM模型主要多了一个DISPATCH状态，用来记录当前SM已经给某个CM发送了本地时钟的情况。注意一个SM对于不同的CM的传输延迟可能不同，所以在SM模型中，对于不同CM其对应的deviation的值也不同，触发dispatch标签的时间也不一致。双CM的模型会根据触发的dispatch标签编号进入对应的DISPATCH状态，然后等待本地时钟值到达触发另一个dispatch标签时进入END状态，代表SM模块已经发送。

图6 双CM的SM模型Fig.6 SM model in a double-CMs network

3.3 触发器模块

为了实现不同的启动模式，本文设计了一个触发器模块TRIGGER。基本思想是通过TRIGGER给当前应启动的SM和CM发送启动标签来模拟不同的启动场景。

同步和异步启动模式下TRIGGER模块的ELTS模型分别如图7(a)和图7(b)所示。触发器一开始处在IDLE状态并等待启动。对于同步启动模式(无论单CM或双CM)，触发器只需向所有的SM和CM以及MONITOR发送一次start标签即可。对于异步启动模式，触发器先转移至WORKING1状态，并向需要先启动的模块发送start标签，然后再向后启动的模块发送later_start标签去触发它们启动。在完成一个完整的同步周期后，通过一个start标签回到WORKING1状态，重新进入启动状态等待新一个同步周期的开始。

(a) 同步启动模式(a) Synchronous model

(b) 异步启动模式(b) Asynchronous mode图7 TRIGGER模型Fig.7 The TRIGGER model

3.4 监视器模块

为了更方便地对协议模型进行验证，设计一个监视器模块MONITOR。MONITOR监测系统中所有SM的本地时钟，并判断其同步精度是否在预先设定的范围之内。

图8 MONITOR模型Fig.8 The MONITOR model

监视器模块的ELTS模型如图8所示。监视器模块包含四个控制状态，分别为：START，SMALL，BIG和BAD。START为初始状态。SMALL表示当前网络处于同步状态，各个SM本地时钟之间的差值应该较小(或者近似相等)，否则监视器进入BAD状态。BIG表示当前网络正在运行时钟同步协议，各个SM本地时钟之间的差值可能较大，但也应该在一个预先设定的范围之内。如果超出该预先设定的范围，监视器也进入BAD状态。

处于START状态的监视器收到start标签后迁移到SMALL状态。从SMALL状态转移到BIG状态需要等待任意一个SM发出dispatchi标签来触发，代表时间同步算法已经启动。TMP状态是为处理双CM模型所设计的临时状态，单CM模型中没有这个状态。处于BIG状态的MONITOR收到CM0发出的agree_sync_0或CM1发出的agree_sync_1标签后转移到TMP状态，继续等待另一个CM发来的agree_sync标签，然后转移至SMALL状态。

MONITOR模块中变量声明为：

int dispatch_num;

int max_drift;

其中，dispatch_num是当前已经发出PCF的SM数量，max_drift是预先设定的用来判断各个SM的本地时钟时间差是否过大的阈值。

MONITOR模块从START状态到SMALL状态的变迁说明为：

from START to SMALL on start do {

dispatch_num = 0;

max_drift = 10;

};

主要执行对MONITOR变量的初始化。

MONITOR模块从SMALL状态到BIG状态的变迁说明为：

from SMALL to BIG on dispatchiprovided

dispatch_num == 0 do {

dispatch_num = dispatch_num + 1;

};

处于SMALL状态的MONITOR收到任一个SM发出的dispatchi标签后触发该变迁，并将dispatch_num的值加1。

MONITOR模块从BIG状态到BIG状态的变迁说明为：

from BIG to BIG on dispatchiprovided dispatch_num > 0 and dispatch_num < CM_amount * SM_amount do {

dispatch_num = dispatch_num + 1;

};

当dispatch_num大于0且小于CM数量乘以SM数量时，每个SM发出的dispatchi都会触发这个变迁并使dispatch_num加1。

MONITOR模块从SMALL状态到BAD状态的变迁说明为：

from SMALL to BAD provided!(SMi.clock==SMj.clock);

其中，“！”表示否定。处于SMALL状态的MONITOR会检测每两个SM之间的本地时钟是否相同。如果存在不同的时钟则会进入BAD状态。

MONITOR模块从BIG状态到BAD状态的变迁说明为：

from BIG to BAD provided (SMi.clock>SMj.clock + max_drift) && (dispatch_num == SM_amount);

处于BIG状态的MONITOR会检测每两个SM之间的本地时钟之差是否超过设定的阈值max_drift。如果存在两个SM之间的时钟差超过max_drift且收到PCF的SM数量dispatch_num等于SM总数SM_amount，则会进入BAD状态。

当验证包含两个CM的系统时需要在BIG状态到SMALL状态的中间加入TMP状态用来接收两个不同CM的时钟同步信号。

MONITOR模块从BIG状态到TMP状态，以及从TMP状态到SMALL状态的变迁说明为：

from BIG to TMP on agree_sync_ido {

dispatch_num = 0;

};

from TMP to SMALL on agree_sync_i;

在双CM的情况下，MONITOR需要收到两个CM完成同步分别发来的标签agree_sync_0和agree_sync_1，才代表整个时钟同步过程结束，因此需要一个中间状态TMP来缓存收到一个agree_sync_i标签的情况。

4 协议验证

4.1 验证属性

为保证时钟同步协议模型的正确性，验证下列两条属性。

4.1.1 时钟误差属性

时钟同步协议的基本目标是保证任何时刻所有SM本地时钟的误差不会超出一个阈值。根据前面对监视器模块的建模，这一属性可以归结为MONITOR模块永远不会到达BAD状态，即

INVARSPEC !(MONITOR.location == BAD)

4.1.2 同步完成属性

除了时钟误差属性外，还需要保证SM和CM运行的时钟同步算法最后都能正常终止，到达终止状态。采用反证法，分别验证

INVARSPEC !(CM.location == CALC)

INVARSPEC !(SM.location == SYNC)

即CM永远不会到达CALC终止状态，SM永远不会到达最终的SYNC状态。如果针对上面两条属性的验证都返回false，说明CM和SM可以到达终止状态，同步完成属性成立。反之，对于任何一条属性的验证返回true，说明对应模块永远不能到达终止状态，同步算法不终止。

4.2 验证环境

本节对4.1小节提到的不同属性，在不同的SM和CM数量配置下进行了验证，试验环境为：Intel(R) Xeon(R) CPU E5-2620 v3 @ 2.40 GHz，32 056 M内存，操作系统为Ubuntu 16.04.2 LTS。

实验采用Beagle[4]执行模型检测。Beagle是清华大学软件学院开发的一个基于ELTS的模型检测工具。Beagle工具中分别基于二叉决策图(Binary Decision Diagram, BDD)和可满足性(SATisfiability, SAT)实现了基本的模型检测方法，并在此基础上，提出了一系列针对构件化系统的高效模型检测算法[7-10]。

4.3 结果分析

对时钟同步协议是否满足时钟误差属性(以下简称P1)和同步完成属性(以下简称P2)进行验证。实验中，根据单CM和双CM的不同启动方式，以及SM的数量分别构建了时钟同步协议的模型，并执行验证。

验证结果如表1所示，其中第1列表示验证的属性，第2列和第3列表示网络中包含的CM和SM数量，第4列为启动模式(第2节中介绍的3种启动模式分别以1，2，3表示)。采用限界模型检测执行验证，第5列表示限界模型检测展开的步数，第6列表示验证所需的时间，第7列表示属性验证的结果。注意属性P1为true、属性P2为false为期望的模型验证结果。

从表1中可以发现，在给定的网络结构下，时钟同步属性和同步完成属性的验证结果都与期望一致。因此时钟同步协议在这些网络结构下的正确性得到验证。另外，可以观察到，验证所需时间与模型展开步数正相关。这是因为当展开步数增加时，整个模型的规模变大，验证所需的时间因此也将增大。

表1 实验结果

5 相关工作

模型检测在协议验证方面得到了广泛的应用,例如路由协议验证、密码协议验证、网络协议验证等。在文献[11]中，Roy等采用概率时间自动机来验证在无线局域网IEEE0802.11协议中的介质访问控制层协议，采用确定路径压缩算法优化模型，减少协议中的冗余，以应对验证中的状态爆炸空间问题。在文献[12]中，Esparza等验证了Population protocol的正确性，该协议是主要应用在传感器网络中的形式化模型,用于在不同设备之间获得一致的值，设备与设备之间通过交互以改变自身状态。在文献[13]中，He等验证了发布订阅分布式协议的正确性。

Steiner和Dutertre等对TTEthernet中的时钟同步协议标准进行了验证[14-16]。他们基于SAL model checker实现了对同步算法的正确性分析，并验证了在协议规定下，系统满足的同步精度范围。与他们的工作相比，本文采用了一种新的建模语言(即扩展标记变迁模型)，建模过程说明了该语言对于时钟同步协议验证的有效性。特别地，本文所建立的模型中考虑了时间触发网络的不同启动模式。该特性是时间触发网络国际标准中没有规定的内容，但却是将时间触发网络引入到我国航空领域某系统的设计中所必须考虑的一个适配性问题。本文结果为该系统的设计提供了可信依据。

6 结论

本文给出了一种基于扩展标记变迁模型对时钟同步协议进行建模的方法，并基于模型检测工具对其正确性进行了验证。除了标准中规定的时钟同步协议外，还对多个启动场景下协议的正确性进行了分析与验证。验证结果证明了在复杂启动场景下时钟同步网络协议的正确性，也表明了扩展标记变迁模型对于协议验证的有效性。