实时模型检测精确加速窗口的计算原理及算法

实时模型检测中，时间自动机可以为实时系统的时间行为进行建模[1].使用时钟描述带有时钟约束的状态迁移，为实时系统的模型检测提供了理论基础[2]，其广泛应用于轮询控制系统、铁路互锁系统等领域.基于时间自动机的模型检测算法，由于引入了时钟变量，控制程序和外界环境通常使用不同的时间度量，可达性分析算法会产生大量状态片段[3-4]，导致状态空间急剧增大，检测时间大幅增长.

加速技术是一种约减方法，可以用来解决由时间度量不同造成的片段问题.文献[5]将加速技术应用到线性目标检测中，可以有效地提高检测性能；文献[6]以隐式Markov模型作为改进框架，对推理模型进行了加速；文献[7]提出了一种新的计算最坏情况执行时间(worst case execution time， WCET)的算法，以时间自动机为模型，使用抽象技术加速了WCET的分析效率；文献[8]基于贝叶斯分类器确定了加速模型，通过分析异质群体的行为趋势，表明加速技术在可靠性评估中能有效提高分析精度；文献[9]介绍了大规模分布式环境中实现目标函数优化的迭代机学习算法，通过平衡性能和效率，使加速效果显著提高；文献[10]利用2个可满足性问题求解器验证在线模型，加速模型检测对复杂行为的处理.

在加速技术的基础上，国内外研究人员设计了很多种优化技术来约减可达性分析所需的存储空间，以解决或者缓解状态空间爆炸问题.文献[11]对时间自动机的时钟采用基于时钟带(zone)的抽象来区分最大上、下界，以获得对可达性验证的完整性.通过此类优化算法，可以有效化简差分矩阵，这将极大地增加实时模型检测工具UPPAAL的可扩展性.文献[12]也研究了时间自动机的可达性问题，通过构建时钟带抽象的搜索树，来模拟自动机状态空间上的底层关系.从有效性的角度考虑，该方法避免了最大上下界方法产生非凸集的潜在可能，使算法更加完备.文献[11-12]采用了时钟带抽象来近似实际可达时钟值，是一种粗粒度方法.时钟带抽象基于符号化方法，根据时间自动机的时钟约束来设置最大上下界抽象的参数.这一类方法对解决可达性问题是健全和完备的，但由于高度的粗粒度抽象，使抽象模型对时间自动机的其他性质无法准确验证.

对于通信协议验证[13]、物联网服务建模[14]等实际问题，精确加速技术是一种更为有效的方法.精确加速技术是一种细粒度的抽象方法，在考虑前向可达性分析的同时，能够分析其他性质的变化及影响.文献[3]利用UPPAAL验证乐高机器人系统时，发现了片段问题并进行简单描述，提出可进一步研究的设想；文献[15]将近似技术运用到实时系统模型的安全性和连通性检测中，可有效控制回路导致重复控制的情况；文献[16]提出一种实时性质语言L∀S来检测可达性中的拒绝状态，同时对模型检测的安全性和边界活性进行了约减.以上文献所提到的问题和方法，促使精确加速的概念提出，为进一步深入研究提供了可能.

在实时模型检测中精确加速方面的研究工作较有代表性的包括文献[17-22].

文献[17]介绍了一种对时间自动机子集的语法调整方法.通过向时间自动机添加1个附加环，能够加速前向符号可达性分析，可有效解决片段问题，对乐高机器人系统出现的问题加速效果明显.但该文献对可加速环窗口的说明不够深入，没有说明窗口大小的计算和进一步约减的办法.文献[18]提出一种基于驻留环实现精确加速的方法，其入口边界条件由可加速环窗口大小决定.由于驻留环的长度固定，其构造的自动机模型更简单，能提高精确加速的速度并降低精确加速的时间和空间开销.该文献同样对可加速环窗口的大小默认为已知，未提及其计算方法.文献[19]通过分析加速过程中的主要参数，提出一种模型检测精确加速的判断方法，推导出了精确加速是否需要的判断条件.该方法可在片段数量较少或片段不满足一定条件时使用，避免添加的附加环降低验证速度.以上工作依赖于特定条件，在实际的实时系统中使用较少，与压缩可加速环规模相比存在一定不足，且对可加速环窗口的概念亦未明确.文献[20]针对时间自动机规模较大的问题，在识别可加速环的方法中引入拓扑排序的思想，提出了一种识别时间自动机中可加速环的方法.通过简化时间自动机的规模，提高了识别时间自动机中可加速环的效率.尽管该方法与本文类似，都对时间自动机的规模进行了简化，但其简化的是非可加速环部分，本文在此基础上对可加速环进行了进一步约减.文献[21]提出了一种利用模型检测技术来提高资源利用率的开发方法，在设计开发阶段，使用了精确加速技术，极大地改进了符号模型检测处理调度系统的能力；文献[22]针对网络物理系统的可调度问题，借助精确加速技术来建模高级规范和验证框架，从而将高级规范自动转换为正式模型.文献[21-22]主要将精确加速技术的思想应用于系统资源调度问题的建模，但并未对原有的精确加速理论进行完善.

精确加速的关键技术是可加速环窗口的计算，向时间自动机添加的附加环和驻留环的参数，都取决于可加速环窗口的大小.上述与精确加速相关的各文献中，给出的实例较为简单，其中可加速环窗口的计算均为人工推演所得，尚未见到有文献提出窗口的计算方法，可加速环窗口的计算成为精确加速中亟待解决的问题.

本文系统地给出了可加速环窗口的定义，并结合实例对窗口计算原理进行分析，根据已有的识别时间自动机中可加速环的方法[20]，提出了一种精确加速中可加速环窗口的计算算法.算法根据窗口计算原理，获取影响窗口大小的有效数据，并对其他无用数据和节点进行约减，压缩了可加速环的规模，提高了计算效率，为精确加速技术的后续实现提供了支持，同时为研发精确加速自动检测程序奠定了基础.

1 基础知识

1.1 时间自动机

为了更清晰地说明时间自动机的实值时钟，首先定义包含所有时钟变量的时钟约束集T(C).假设时钟变量集为C，时钟约束τ的定义为

其中c∈C，n∈N，?表示二元关系{<,≤,=,≥,>}中的一种.时钟约束集T(C)是时钟约束τ的集合.

时钟解释v是从C到R+∪{0}的1个映射，R+为正实数集，即为时钟变量集C中的每个时钟变量赋值.对于时钟变量集C的子集X，X width=13,height=13,dpi=110

0表示X的所有时钟变量c赋值为0(时钟复位)，而对集合C-X的时钟变量没有影响.

定义1. 时间自动机[23].时间自动机定义为1个六元组(C,L,l0,A,I,E).其中C是时钟变量集，L是有穷的状态位置集合，l0∈L是起始位置，A是有穷的动作事件集合，I是使每一个状态位置l∈L都有1个时钟约束的映射，E⊆L×A×T(C)×2C×L是边界的规则转换集合.1个规则转换(l,a,τ,λ,l′)表示：当状态位置l的时钟满足时钟约束τ，则系统可以完成动作事件a从状态位置l转移到状态位置l′，并完成λ中的全部时钟复位.

图1是时间自动机定义示例，时间自动机M表示对实时系统中控制程序和外部环境的简易抽象建模.状态位置l1，l2，l3组成的环表示对控制程序的建模，称之为控制环，时钟为x；对外部环境的建模由时钟y所体现，每次转换到状态位置l2时检验y，若满足y≥LARGE，则跳出控制环.

1.2 前向符号可达性分析

前向符号可达性分析算法是实时模型检测工具UPPAAL的核心之一.模型检测引擎运用on-the-fly算法策略，从起始位置开始进行前向搜索，判断某个符号状态空间是否可达.对于每一个尚未搜索的符号状态，需要根据其时钟和动作计算出后继状态，并与已搜索的符号状态作比较.若已经出现，则舍弃；若没有出现，则将该后继状态添加到已搜索的符号状态列表中.

为了进一步说明前向符号可达性分析过程，以图1时间自动机M为例，表1给出了时间自动机M从起始位置开始进行前向符号搜索，执行1次控制环后得到的符号状态，表格结果由UPPAAL模拟器得到.表1中，符号状态6与符号状态3虽然状态位置都是l2，但是由于二者的时钟带不同，所以是两种不同的符号状态，需要进一步前向搜索符号状态6.符号状态5与符号状态2亦同理.由此可知，每执行一次控制环，总能得到新的符号状态.

由于阈值LARGE通常较大，而时钟y的增长较为缓慢，当验证l4的可达性时，时间自动机M需要执行若干次控制环才能使时钟y得到有效地增长，而执行次数的多少取决于LARGE的值.LARGE值越大，执行的次数越多.正是由于建模中出现的不同时钟，时间自动机在符号模型检测时，运用时钟带抽象技术[11-12]，状态空间会出现大量不必要的时钟带片段，形成前向符号搜索片段问题.

1.3 可加速环

与数学中的环(ring)不同，时间自动机中的环(cycle)可以简单理解成一组边及其所经过位置的序列，而序列的起始和终结位置是同一位置.可加速环是一类定义较为严格的环，环中的时钟约束(包括状态位置的时钟约束、边界的时钟约束和时钟复位)只能包含1个时钟.具体定义为:

定义2. 可加速环[17].给定1个时间自动机M=(C,L,l0,A,I,E)，设Ecyc=(e0,e1,…,en-1)∈En且x∈C，则可加速环定义为二元组(Ecyc,x)，满足的条件为：

1) Ecyc是1个环；

2) 对于Ecyc中出现的所有状态位置l，其时钟约束I(l)为空或者是{x≤c}的形式；

3) 设(l,a,τ,λ,l′)∈Ecyc，其边界时钟约束τ为空或者是{x≥c}的形式，时钟复位λ为空或者只含有x；

4) x必须在Ecyc的重置位置src(e0)的全部入边上复位.

这里的时钟x命名为环时钟，时钟约束I(l)命名为位置不变式，时钟约束τ命名为边界约束.重置位置src(e0)表示可加速环外部时钟的检测位置，且该位置的出边为e0；若环中某个状态位置的入边为ei，则该位置的出边为ei+1，其中i∈[0,n-2].

图1中时间自动机M的状态位置l1，l2，l3组成的控制环就是1个可加速环，环时钟为x，重置位置为l2.各个状态位置的位置不变式及环内各条边的边界约束都满足可加速环的时钟约束形式，在l2的唯一入边，环时钟x复位为0.

2 可加速环窗口

每个可加速环都有1个窗口，它的含义是指自动机执行1次可加速环，环内时钟增加大小的区间.

定义3. 可加速环窗口.设时间自动机M中的1个可加速环为(Ecyc,x)，其所有轨迹的压缩序列表示为

其中νi和

都表示1条时钟解释，i∈[0,n]；l0=ln=src(e0)，均表示重置位置；

取决于边em，可理解为em的动作事件迁移，m∈[0,n-1].设边em即轨迹序列

的迁移时延为Dm，则TRACE(Ecyc)的总时延

可加速环(Ecyc,x)的窗口定义为区间[a,b]，a，b∈N，满足的条件为：

2) 对任意实数d∈[a,b]，都可以在合法时钟约束下调整TRACE(Ecyc)中的每个时延Dm，使D为d.

定义中总时延的含义，即为环内时钟的增加量，可以根据定义理解为：时间自动机从重置位置开始，执行1次可加速环回到重置位置时外部时钟的增加量.窗口即环内时钟增量区间.

定理1. 设时间自动机M中的1个可加速环为(Ecyc,x)，环内各节点集合Lcyc={li|li=src(ei)且0≤i≤n-1}，li=src(ei)表示li节点位置是边界ei的起始节点.对任意节点li，若外部时钟为y，则第2次回到该节点时，时钟带y-x的增量区间[a′,b′]等于环内时钟增量区间，而不必考虑是否已从重置位置进入了可加速环.区间[a′,b′]是可加速环(Ecyc,x)的窗口.

证明. 分2种情况进行讨论.若已从重置位置进入了可加速环，根据对定义的分析，环内各组件对外部时钟的影响范围相同，并在重置位置入边上时钟复位，所以各节点位置的时钟带x固定，不妨设节点li的时钟带xi∈[x1,x2]，x1，x2∈N.又因为任意节点执行可加速环1次其外部时钟y的增量区间等于环内时钟增量区间，设可加速环窗口为[a,b]，第1次经过节点li的时钟带yi∈[y1,y2]，第2次经过节点li的时钟带

N，所以有a=y3-y1，b=y4-y2.节点li的时钟带y-x的增量区间为[a′,b′]，则a′=(y3-x1)-(y1-x1)，b′=(y4-x2)-(y2-x2)成立.所以a=a′，b=b′，故区间[a′,b′]是可加速环窗口.

若尚未从重置位置进入可加速环，根据对定义3的分析，外部时钟y的增量区间与环内时钟增量区间存在的偏差δ主要取决于进入可加速环前的时钟数据.而由于没有进入可加速环，环时钟x和外部时钟y是一样自然增长的，均可看作全局时钟，节点li的时钟带y-x可以完全去除偏差δ.偏差δ一旦去除，节点li就等同于提前进入可加速环.以此为起点再回到这个节点时，时钟带y-x表示的就是外部时钟在环内的净增长，时钟带y-x的增量区间与环内时钟增量区间等价，即为窗口.

综合上述2种情况可知定理1成立.

3 精确加速窗口的计算原理及算法

3.1 计算原理

根据可加速环的定义，窗口计算的是环内时钟增量，需要观察到达环内同一状态位置执行可加速环前后的时钟变化.因此，可加速环窗口的计算可以从前向符号搜索得到的符号状态入手.仍以图1为例，根据时间自动机的语义，具体分析精确加速的计算原理，总结可加速环窗口的一般计算方法.

时间自动机M在起始位置l0时，环时钟x和外部时钟y初值为0；

M转移到状态位置l1，x至少增长到大于3才会转移，而l1的位置不变式要求x≤5，因此到达l1时，3<x≤5，y与x的增长相同，3<y≤5；

M转移到状态位置l2，边界约束为x≥3，同时x时钟复位，l2的位置不变式为x≤2；到达l2时，x的变化范围取决于时钟复位和位置不变式，0≤x≤2；y的增长区间Δy取决于边界约束和上一位置x的范围以及位置不变式，边界约束x≥3和上一位置3<x≤5说明Δy≥0，位置不变式x≤2说明Δy≤2，又有上一位置3<y≤5，则3<y≤7；判断此时y是否大于等于LARGE，判断为否，M进入可加速环；

M转移到状态位置l3，x时钟复位，l3的位置不变式为x≤4，因此到达l3时，0≤x≤4；因为没有边界约束，而上一位置0≤x≤2，所以Δy≥0，由位置不变式知Δy≤4，又有上一位置3<y≤7，则3<y≤11；

M转移到状态位置l1，边界约束为x≥1，l1的位置不变式为x≤5；到达l1时，因为没有时钟复位，此时x的变化范围取决于边界约束和位置不变式，1≤x≤5；对于y，边界约束x≥1和上一位置0<x≤4说明Δy≥1，因为没有时钟复位，Δy的上界不仅要考虑位置不变式，还要考虑与上一位置的位置不变式的差异，l1位置不变式x≤5，l3位置不变式x≤4，因此Δy≤1，故Δy=1，又有上一位置3<y≤11，则4<y≤12；

M转移到状态位置l2，边界约束为x≥3，同时x时钟复位，l2的位置不变式为x≤2，到达l2时，0≤x≤2；边界约束x≥3和上一位置1≤x≤5说明Δy≥2，位置不变式x≤2说明Δy≤2，故Δy=2，又有上一位置4<y≤12，则6<y≤14；可加速环完整执行一次，判断此时y是否大于等于LARGE，判断为否，M第2次进入可加速环.

M再次执行可加速环的分析过程与之前相类似，环时钟x和外部时钟y的变化主要取决于位置不变式、边界约束、时钟复位3个因素.对于环时钟x，若存在时钟复位，则x的变化范围取决于时钟复位和位置不变式，否则其变化范围取决于边界约束和位置不变式；对于外部时钟y，主要考察Δy的变化范围，其下界取决于边界约束和上一位置x的范围，其上界取决于位置不变式.经分析，可加速环内的x与Δy的取值范围是始终不变的.总结上述分析过程，表2给出了时间自动机M执行2次可加速环得到的符号状态.

通过对比表2和表1的数据发现，分析结果的前6个状态与UPPAAL模拟器得到的结果是一致的，说明分析过程合乎规范.

根据可加速环窗口的定义，选取重置位置l2的2个符号状态3，6的时钟带y计算窗口，从3<y≤7到6<y≤14的时钟增量为[3,7]，因此窗口为[3,7].同理亦可选择符号状态4，7或符号状态5，8的时钟带y计算窗口，其实质均是计算环内Δy的取值.

根据定理1，更快计算窗口的方法是选取符号状态2、5，直接计算时钟带y-x的增量区间.从y-x=0到3<y-x≤7的时钟增量为[3,7]，因此窗口为[3,7].2种方法得到的结果一致，而后者需要搜索的符号状态更少.

3.2 计算算法

根据对窗口计算原理的分析，窗口的计算取决于位置不变式、边界约束、时钟复位3个因素.为了使算法的描述更简便，设cnL和cnE分别表示位置不变式和边界约束中的常量，定义其自然数的提取规则为：

1) 当I(l)=∅时，cnL(I(l))=∞；当I(l)={x≤c}时，cnL(I(l))=c；

2) 当τ=∅时，cnE(τ)=0；当τ={x≥c}时，cnE(τ)=c.

文献[20]给出了识别时间自动机中可加速环的方法，对图1中的时间自动机M使用文献给出的方法处理后，得到如图2所示的可加速环(Ecyc,x).

可加速环窗口的计算，可以选择环中任意入边有环时钟复位的节点作为起始，结合可加速环的定义和精确加速的原理分析，对识别出的可加速环进行进一步精准压缩，减少环中节点数量，提高计算速度.精确加速中可加速环窗口的计算算法为：

Step1. 对于时间自动机M，使用识别时间自动机可加速环算法[20]，输出M中所有可加速环.

Step2. 选取1个未处理的可加速环，选择环中任意入边有环时钟复位的节点作为起始，检测其出边是否有环时钟复位.若有则记录这一节点，若无则不记录，然后转移到下一节点继续检测，直到回到起始节点.

Step3. 若记录的节点个数与该可加速环节点个数相同，则可加速环无需压缩，计算窗口使用原环，转Step6，否则执行Step4.

Step4. 将所记录的节点按照记录顺序连接成1个新环，各节点的位置不变式与原环一致，新环所有边均含有环时钟复位，各边边界约束的计算执行Step5.此时得到节点压缩后的新可加速环，计算窗口使用新环.

Step5. 求新环各边的边界约束.不妨设所求边的起始节点为A，A在新环中其入边的起始节点为B.首先在原环中找出一条从B到A的转移路径，然后计算出转移路径中除节点B以外各节点出边cnE(τ)值较大的，其边界约束作为所求边的边界约束.

Step6. 计算可加速环窗口[a,b].a为各边cnE(τ)之和，b为各节点cnL(I(l))之和.

Step7. 若仍有未处理的可加速环，转Step2，否则算法结束.

伪代码表示为：

算法1. 计算可加速环(Ecyc,x)的窗口[a,b].

输入：可加速环(Ecyc,x)；

输出：窗口边界a和b.

Ecyc=(e0,e1,…,en-1)，且对于每一个ei有ei=(li,ai,τi,λi,li+1)；

① function WindowComputation(Ecyc,x)

③ KEY[0,1,…,n]←0;

④ for i←0 to n-1 do

⑤ if λi≠∅ then

⑥ reset←reset+1;

⑩ A[1,2,…,reset]←0;

B[1,2,…,reset]←0;

for j←1 to reset do

A[j]←MaxCount(KEY[0,1,…,n],j);

B[j]←cnL(I(lKEY[j]));

for j←1 to reset do

function MaxCount(KEY[0,1,…,n],j)

for i←KEY[j-1]+1 to KEY[j] do

if cnE(τi)>max then

若可加速环节点数量为n，则算法1的Step2～Step3的时间复杂度为O(n)，算法1的Step4～Step5的时间复杂度为O(n)，算法1的Step6的时间复杂度最差为O(n)；考虑到算法1的Step1调用文献[20]识别时间自动机可加速环算法的时间复杂度为O(n2)，因此整个算法的时间复杂度为O(n2).

因为可加速环的定义要求时钟x必须在重置位置的全部入边上复位，所以至少有λn-1非空，reset至少为1，算法的后续计算依托于reset值；而可加速环的定义又严格要求了位置不变式、边界约束、时钟复位的出现形式，因此该算法必然有解.

定理2. 设时间自动机M中的1个可加速环为(Ecyc,x)，环内各节点集合Lcyc={li|li=src(ei)且0≤i≤n-1}.采用可加速环节点压缩算法生成的新可加速环，其可达性与原可加速环(Ecyc,x)等价.

证明. 在时间自动机的验证过程中判断某个状态是否可达，可以对实时系统的安全性等性质进行验证.假设位置r可达，那么含有位置r的位置s也是可达的，r，s∈Lcyc.时间自动机M的目标位置集合LF⊆L蕴含了可达性判定，若要证明节点压缩前后的可加速环的可达性等价问题，需要构造位置之间等价关系的有穷商.假设原可加速环有节点p∈Lcyc，新可加速环有节点

且

如果p～q且

那么存在节点q′使得

且有q′～p′.由于等价关系的稳定性，考虑的2个等价类Π和Π′，分别包含节点p和q.对某个

当且仅当对Π中每个p都存在p′∈Π′，使得

等价关系～的有穷商是～的稳定划分，对某个q∈Π′和q′∈Π，有穷商包含

由于节点压缩前后的可加速环其重置位置固定不变，即等价类包含相同的初始位置，则有穷商包含动作事件为a的从等价类Π到Π′的转换.

现利用所提出的算法计算图2可加速环(Ecyc,x)的窗口[a,b]：

因为时钟x在各边上时钟复位2次，所以reset=2，需要记录的节点有l1，l2，所构造的新环比原环减少1个节点；原环被分为2部分，一部分是l2及其出边，剩余的是另一部分；新环各边均包含时钟x复位，边界约束τ依次为空和x≥3(即A[1]=max{0}=0，A[2]=max{1,3}=3)，位置不变式I(l)依次为x≤2和x≤5(即B[1]=cnL(I(l2))=2，B[2]=cnL(I(l1))=5).此时，节点压缩后的新可加速环构造完成，如图3所示：

计算a为各边cnE(τ)之和，a=A[1]+A[2]=3；b为各节点cnL(I(l))之和，b=B[1]+B[2]=7.所以可加速环的窗口为[3,7]，与之前的分析结果一致.

4 实验结果

通过与物联网科研团队的交流及合作，精确加速技术成功已应用于物联网网关安全系统的建模及验证中[24].图4展示了物联网网关安全系统的核心部分——轮询模块的时间自动机模型.对于轮询模块，通过同步通道开启轮询，并由类型状态控制轮询逻辑的终端是感知终端还是执行终端，使用不同的流程进行处理.物联网网关安全系统的核心技术是基于时间标签的AES密码算法[25]，通过在密钥扩展阶段引入时间标签，使轮密钥可随时间的变化进行动态更新，进而实现密文的变化，有效地保证机密信息的安全性.由于引入了时间标签，使得系统产生了可加速环，精确加速技术的应用可有效提升验证效率.

对物联网网关安全系统使用3.2节算法进行分析，首先识别出系统中若干个可加速环，以其中1个可加速环为例，如图5所示：

然后对可加速环进行处理，构造节点压缩后的新环，所有边均含有环时钟复位.新环如图6所示：

最后进行可加速环窗口的计算，仅需遍历各新环的位置不变式和边界约束即可.计算cnE(τ)之和为窗口下限，计算cnL(I(l))之和为窗口上限，因此可加速环窗口为[6,10].结果经过UPPAAL模拟器验证无误.

对物联网网关安全系统中的所有可加速环使用3.2节算法进行节点压缩处理，再次验证系统的机密性、可用性、真实性、顽健性、完整性、新鲜性等性质，实验结果如表3所示:

对于未处理系统，首先需要执行节点压缩算法，然后再验证有关安全性质，执行压缩算法所需消耗的时空资源如表4所示:

实验结果表明，节点压缩后的物联网网关安全系统模型验证时间(含节点压缩算法时间)平均减少了8.04%，内存消耗(含节点压缩算法内存)平均减少了26.87%，且精简后的时间自动机模型没有影响到相关性质的验证.

此外，所提出的算法还可以快速检索出模型中的死锁问题，以图7时间自动机M′为例.

对时间自动机M′使用3.2节的算法进行分析，首先可以识别出4个可加速环，如图8所示.各个环中的位置不变式、边界约束、时钟复位均可为空.

对每一个可加速环进行处理，构造节点压缩后的新环，其严格满足可加速环定义，且所有边均含有环时钟复位.4个可加速环压缩后的新可加速环如图9所示.

需要注意的是对于新可加速环3，l14→l13的迁移是无法执行的.因为l14的位置不变式x≤7与边界约束x≥8相互矛盾，此时环进入死锁状态.还原到时间自动机M′中，死锁状态同样存在.相比于原自动机模型，压缩后的新环更容易发现死锁状态的存在.舍弃掉存在死锁的可加速环，时间自动机M′实际只有3个可以执行的可加速环(即可加速环1，2，4).

最后，可加速环窗口的计算，仅需遍历各新环的位置不变式和边界约束即可.计算cnE(τ)值之和为窗口下限，计算cnL(I(l))值之和为窗口上限.容易得到可加速环1，2，4的窗口分别为[7,18]，[6,16]，[13,24].经过UPPAAL模拟器的验证可知，所得结果正确无误.

通过该实例可知，包含节点状态多的环，其窗口不一定比节点状态少的环大，如可加速环1和2；只要1个环满足可加速环定义，就可以进一步压缩成1个所有边均含有环时钟复位的新可加速环，而不论其是否存在死锁，如可加速环3；1个可加速环存在死锁，并不能说明整个时间自动机进入死锁，可能有其他路径可以迁移，如可加速环3和4.

5 总结与展望

通过对精确加速技术核心——可加速环的分析，阐释了其关键技术可加速环窗口计算的必要性，而目前均为人工推演，缺少严格的数学推导；运用识别时间自动机中可加速环的方法，提出了一种精确加速中可加速环窗口的计算方法，并结合具体实例进行了分析.主要工作有：

1) 提出一种精确加速窗口的计算方法，算法压缩了可加速环的节点规模，使计算模型更为简单，窗口的计算效率得到了提高，同时能够发现模型死锁等问题；

2) 结合物联网网关安全系统模型等实例，从时空损耗的角度对系统的性质进行验证，实验结果表明了算法的高效性.

在对复杂实时系统进行建模时，可能会出现多个可加速环叠加在同一位置的情况.运用附加环技术进行精确加速，所添加的位置会由于可加速环数量的增加而成倍增长，进而导致内存不足无法进行模型检测；运用驻留环技术进行精确加速，多个可加速环的叠加使得驻留环入口条件不统一，而对于某一个驻留环，仍需执行其对应的可加速环a width=4,height=14,dpi=110

(b-a)次，多个可加速环窗口的差异会使时间消耗大幅增加.如何解决复杂实时模型中的精确加速，是下一步需要重点研究的工作.另外，利用算法压缩可加速环节点的思想，尝试将原自动机模型整体精简，在保证其原有性质的同时快速检测死锁等问题；综合应用窗口计算、添加附加环和驻留环等方法，并结合实际问题将动作迁移、紧急通道等其他条件考虑在内，尝试搭建简单的精确加速自动检测平台，也是下一步研究的主要工作.

[1]Pinisetty S, Jéron T, Tripakis S, et al. Predictive runtime verification of timed properties[J]. The Journal of Systems and Software, 2017, 132: 353-365

[2]Han Deshuai, Yang Qiliang, Xing Jianchun. UML-based modeling and formal verification for software self-adaptation[J]. Journal of Software, 2015, 26(4): 730-746 (in Chinese)(韩德帅, 杨启亮, 邢建春. 一种软件自适应UML建模及其形式化验证方法[J]. 软件学报, 2015, 26(4): 730-746)

[3]Iversen T K, Kristoffersen K J, Larsen K G, et al. Model-checking real-time control programs: Verifying LEGO MINDSTORMS systems using UPPAAL[C] //Proc of the 12th Euromicro Conf on Real-Time Systems. Piscataway, NJ: IEEE, 2000: 147-155

[4]Chen Haiming, Cui Li. Design and model checking of service oriented software architecture for Internet of things: A survey[J]. Chinese Journal of Computers, 2016, 39(5): 853-871 (in Chinese)(陈海明, 崔莉. 面向服务的物联网软件体系结构设计与模型检测[J]. 计算机学报, 2016, 39(5): 853-871)

[5]Dubout C, Fleuret F. Accelerated training of linear object detectors[C] //Proc of the 2013 IEEE Conf on Computer Vision and Pattern Recognition Workshops. Piscataway, NJ: IEEE, 2013: 572-577

[6]Jeong H, Yoo Y, Yi K M, et al. Two-stage online inference model for traffic pattern analysis and anomaly detection[J]. Machine Vision and Applications, 2014, 25(6): 1501-1517

[7]Al-Bataineh O, Reynolds M, French T. Accelerating worst case execution time analysis of timed automata models with cyclic behavior[J]. Formal Aspects of Computing, 2015, 27(5/6): 917-949

[8]Lin Kunsong, Chen Yunxia, Xu Dan. Reliability assessment model considering heterogeneous population in a multiple stresses accelerated test[J]. Reliability Engineering and System Safety, 2017, 165: 134-143

[9]Wang Junxiong, Wang Hongzhi, Zhao Chenxu, et al. Iteration acceleration for distributed learning systems[J]. Parallel Computing, 2018, 72: 29-41

[10]Qanadilo M, Samara S, Zhao Yuhong. Accelerating online model checking[C] //Proc of the 6th Latin-American Symp on Dependable Computing. Piscataway, NJ: IEEE, 2013: 40-47

[11]Behrmann G, Bouyer P, Larsen K G, et al. Lower and upper bounds in zone-based abstractions of timed automata[J]. International Journal on Software Tools for Technology, 2006, 8(3): 204-215

[12]Herbreteau F, Srivathsan B, Walukiewicz I. Better abstractions for timed automata[J]. Information and Computation, 2016, 251: 67-90

[13]Zhang Fengling, Bu Lei, Wang Linzhang, et al. Modeling and analysis of wireless sensor network protocols by stochastic timed automata and statistical model checking[J]. SCIENTIA SINICA Informationis, 2013, 43(1): 90-107 (in Chinese)(张凤玲, 卜磊, 王林章, 等. 基于随机时间自动机和统计模型检验技术的无线传感网络协议建模与分析[J]. 中国科学:信息科学, 2013, 43(1): 90-107)

[14]Li Ge, Wei Qiang, Li Lixing, et al. Environment based modeling approach for services in the Internet of things[J]. SCIENTIA SINICA Informationis, 2013, 43(10): 1198-1218 (in Chinese)(李戈, 魏强, 李力行, 等. 物联网服务建模:一种基于环境建模的方法[J]. 中国科学: 信息科学, 2013, 43(10): 1198-1218)

[15]Möller M O. Parking can get you there faster: Model augmentation to speed up real-time model checking[J]. Electronic Notes in Theoretical Computer Science, 2002, 65(6): 202-217

[16]Aceto L, Bouyer P, Burgue width=5,height=6,dpi=110

o A, et al. The power of reachability testing for timed automata[J]. Theoretical Computer Science, 2003, 300(1/2/3): 411-475

[17]Hendriks M, Larsen K G. Exact acceleration of real-time model checking[J]. Electronic Notes in Theoretical Computer Science, 2002, 65(6): 120-139

[18]Yin Chuanlong, Zhuang Lei, Wang Congyin. Exact acceleration of real-time model checking based on parking cycle[J]. Acta Electronica Sinica, 2011, 39(3): 489-493 (in Chinese)(尹传龙, 庄雷, 王从银. 实时模型检测中基于驻留环的精确加速[J]. 电子学报, 2011, 39(3): 489-493)

[19]Gou Lijie, Li Zhen, Wang Congyin, et al. A method to determine the exact acceleration efficiency in model checking[J]. Journal of Zhongyuan University of Technology, 2014, 25(4): 37-41 (in Chinese)(勾利杰, 李真, 王从银, 等. 一种模型检测精确加速的判断方法[J]. 中原工学院学报, 2014, 25(4): 37-41)

[20]Yin Chuanlong, Song Wei, Zhuang Lei. Method of acceleratable cycles in identify timed automata[J]. Computer Engineering and Design, 2010, 31(23): 5113-5115, 5132 (in Chinese)(尹传龙, 宋伟, 庄雷. 识别时间自动机中可加速环的方法[J]. 计算机工程与设计, 2010, 31(23): 5113-5115, 5132)

[21]Boudjadar A, David A, Kim J H, et al. Statistical and exact schedulability analysis of hierarchical scheduling systems[J]. Science of Computer Programming, 2016, 127: 103-130

[22]Chadli M, Kim J H, Larsen K G, et al. High-level frameworks for the specification and verification of scheduling problems[J]. International Journal on Software Tools for Technology Transfer, 2017, 20(4): 397-422

[23]Alur R, Dill D L. A theory of timed automata[J]. Theoretical Computer Science, 1994, 126(2): 183-235

[24]Wang Guoqing, Zhuang Lei, Wang Ruimin, et al. Modeling and verifying based on timed automata of Internet of things gateway security system[J]. Journal on Communications, 2018, 39(3): 63-75 (in Chinese)(王国卿, 庄雷, 王瑞民, 等. 基于时间自动机的物联网网关安全系统的建模及验证[J]. 通信学报, 2018, 39(3): 63-75)

[25]Yin Aihan, Wang Shengkai. A novel encryption scheme based on timestamp in gigabit ethernet passive optical network using AES-128[J]. Optik, 2014, 125(3): 1361-1365