实时系统是指这样的一类计算机应用系统, 它要求在一定时限内及时的响应外部事件, 并在一定时限内完成事件的处理. 在这类系统中, 确保其准确性和可靠性非常重要, 一旦出现缺陷, 带来的经济财产损失都是巨大的. 实时系统的模型检测^[1]是确保实时系统的可靠性和正确性的一种重要技术, 它通过遍历状态空间寻找是否存在不满足规约的状态或路径来验证系统是否正确可靠.

时间自动机模型是实时系统最广泛使用的一种数学模型, 针对实时系统的模型检测工具主要采取时间自动机作为形式模型, 以计算树逻辑 (Computation Tree Logic, CTL)^[1]或线性时序逻辑(Linear Temporal Logic, LTL)^[1]作为性质描述语言. 典型的代表有UPPAAL、KRONOS、RED以及CTAV等.

CTAV^[2]是中科院软件所在2009年实现的一个关于时间自动机的符号化模型检测工具, 在关于时间自动机的模型检测中它是第一个针对线性时序逻辑LTL的模型检测工具, 它先将时间自动机关于LTL的模型检测化归为时间Büchi自动机的空性检测, 然后文献[2]中证明了时间Büchi自动机的空性检测可通过zone抽象化归为Büchi自动机的空性检测, 这样就可以利用Büchi自动机的空性检测算法来完成时间自动机关于LTL的模型检测. 基于这一方法, 文献[3]最早实现了时间自动机关于LTL的符号化模型检测, 这里符号化的含义是指模型检测使用的是时间自动机的基于zone的符号化语义. 文献[2]中使用的Büchi自动机的空性检测算法是单线程的. 2013年, 文献[4–7]在其多核模型检测工具LTSmin的基础上利用文献[2]中的方法实现了时间自动机关于LTL的多核模型检测工具LTSmin+opaal, 使得验证效率有了较大的提高. 与此同时捷克人在他们的多核模型检测工具DIVINE3.0^[8,9]中也实现了时间自动机关于LTL的多核模型检测. 本文我们将在文献[10–12]中给出的关于Büchi自动机的多核模型检测算法的基础上在CTAV工具中实现时间Büchi自动机关于LTL的多核模型检测, 与LTSmin+opaal和DIVINE3.0相比, 在系统描述语言方面, 我们工具支持比时间自动机表达能力更强的时间Büchi自动机, 其它两个只支持时间自动机模型, 这一点对证明活性性质至关重要, 在性质描述语言方面, 由于CTAV本身可以支持LTL的实时扩展MTL_{0, ∞} (Metric Temporal Logic)^[3], 所以我们的工具将能比其它两个工具支持更多的性质验证.

本文的主要内容如下: 研究了多种Büchi自动机的多核空性判定算法, 基于文献[10–12]实现时间Büchi自动机关于LTL的多核模型检测, 同时对比了多种多核算法在CTAV工具下的效果, 并基于符号化状态之间的包含关系给出了一种优化方法, 并最终对比了divine的实验结果.

1 基本概念 1.1 时间自动机

时间自动机^[13]就是带有时钟集的有限自动机. 时钟集是有限个时钟的集合, 每个时钟都是一个取值为非负实数的变量. 时间自动机状态之间的转换要满足时钟约束才可能发生. 时间自动机的状态可以附加上“节点不变量”的属性, 这也是一个时钟约束, 用来保证状态不会保持在原地不动.

时间自动机的形式化定义^[14]是一个六元组M=<L, l₀, Σ, X, Inv, E>, 其中,

(1) X为时钟变量的有限集合, C(X)为X上时钟约束的集合, 其定义为:

$\psi :: = {\rm{ }}true{\rm{ }}\left| {{\rm{ }}x\sim c{\rm{ }}} \right|\psi 1 \wedge \psi 2$

其中, x $ \in $ X, ~ $ \in $ {<, ≤, ==, >, ≥},c是非负整数.

(2) L是节点的非空有限集合, l₀ $ \in $ L是初始节点.

(3) $Inv:L \mapsto C(X)$ 为每个节点指定时钟约束, 称为节点不变量.

(4) Σ为标号的有限集合.

(5) $E \in L \times C(X) \times \sum \times {2^X} \times L$ 是迁移的集合. 迁移(l₀, g, a, Y, l₁) $ \in $ E表示在满足约束条件g的前提下, 通过标号为a $ \in $ Σ的迁移, 可以从节点l₀迁移到它的后继节点l₁, 同时, 时钟集 $Y(Y \subseteq X)$ 中的时钟被重置为0.

时间自动机M的迁移动作主要包含2种, 分别是延迟迁移和离散迁移.

1.2 Zone^[15]

假设X为时钟变量的有限集合, Φ(X)为时钟变量集合X上扩展时钟约束的集合, 扩展时钟约束的语法定义如下:

$\psi :: = {\rm{ }}true{\rm{ }}\left| {{\rm{ }}x\sim c{\rm{ }}} \right|{\rm{ }}x{\rm{ }} - y\sim c{\rm{ }}|\psi 1 \wedge \psi 2$

式中: x, y $ \in $ X, ~ $ \in $ {<, ≤, >, ≥},c是非负整数. 对于时钟赋值u, u 满足扩展的时钟约束的充分必要条件是在赋值u下为真.

Zone通常用DBM (Difference Bound Matrices)^[16]来表示.

DBM是一个矩阵, 矩阵中的每一个元素是一组时钟的两两差值. 其定义了一个值为0的绝对时钟, 对于DBM D中的元素D_ij表示其中的第i行第j列, 它表示zone中时钟变量i和时钟变量j形成的时钟约束.

例如, 一个时钟区域x≥6∧0≤y≤3∧y≤x–1, 引入绝对时钟后可以将表达式改写成0–x≤–6∧0–y≤0∧y–0≤3∧y–x≤–1, 用3×3矩阵表示, 分别为:

$\left[ {\begin{array}{*{20}{c}}{0 - 0 \le 0}&{0 - x \le - 6}&{0 - y \le 0}\\{x - 0 \le {\rm {INF}}}&{x - x \le 0}&{x - y \le {\rm {INF}}}\\{y - 0 \le 3}&{y - x \le - 1}&{y - y \le 0}\end{array}} \right] {\text{和}}$

$\left[ {\begin{array}{*{20}{c}}{ \le 0}&{ \le - 6}&{ \le 0}\\{ \le {\rm {INF}}}&{ \le 0}&{ \le {\rm {INF}}}\\{ \le 3}&{ \le - 1}&{ \le 0}\end{array}} \right],$

其中INF表示无穷大.

1.3 符号化语义

假设D表示一个zone, Y是时钟集合, 对其延迟和重置定义如下:

D↑={u+d|u $ \in $ D, d $ \in $ R^≥0}, 表示zone的延迟定义;

r(D)={u[Y:=0]|u $ \in $ D}, 表示zone的重置.

时间自动机(如图1)的符号化状态是(l, D), l是节点, D是zone. 初始状态 $(l_0, D_0 \uparrow \wedge Inv(l_0))$ , l₀是初始节点, D₀表示所有时钟都为0.

时间自动机的符号化语义为以(l, D)为状态的迁移系统, 迁移 $(l', D')\xrightarrow{a}(l'', D'')$ , 如果有(l, g, a, Y, l₁) $ \in $ E, 并且 $D'' = ((D' \wedge g)[Y: = 0] \wedge Inv(l'')) \uparrow \wedge Inv(l'')$ , D''不为空.

图1中的时间自动机在符号化语义下的一个可能迁移序列如下:

(start, x>=0∧y>=0∧x=y) →

(loop, 0<=x<=100∧0<=y<=100∧y=x) →

(loop, 0<=x<=100∧100<=y<=200∧y=x+100) →

(loop, 0<=x<=100∧200<=y<=300∧y=x+200) →

(loop, 0<=x<=100∧300<=y<=400∧y=x+300) →

(end, x>=0∧y>=300∧y=x+300)

其中loop表示自循环迁移, 并且这个迁移前后的状态不相同, 这个迁移系统有无穷多个状态.

2 原理 2.1 模型检测

给定时间自动机M=(L, l₀, Σ, x, I, E)和LTL公式φ, 要检验LTL性质是否被时间自动机M所满足. 在文献[2]中提出了一种检测算法, 主要思路是先将公式¬φ转化为一个Büchi自动机M¬φ, 然后检验M与M¬φ的合成M‖M¬φ是否为空, 这样将LTL性质的检验转换为对M‖M¬φ的空性判定, 而对此类空性判定, 通过使用基于zone的符号化语义将M‖M¬φ转化成一个Büchi自动机, 然后利用Büchi 自动机空性检测算法来完成.

将检验LTL性质是否被时间自动机所满足转换为对Büchi自动机空性检测的结果, 若空性检测的结果为空, 则性质被自动机M所满足; 反之若空性检测的结果不为空, 则性质不被自动机M所满足.

2.2 符号化状态

在符号化状态抽象表示过程中, 状态的表示我们是采取DBM来表示的, 因此状态之间会产生集合的包含关系, 在状态展开的遍历过程中我们采取判断状态是否遍历过或者已经在被删除状态集合中来对其进行后续处理, 在文献[4]中我们得到以下引理.

引理1. 在状态空间中如果有 $S_k \subseteq S_j$ , 并且S_k可以到达接受环, 那么S_j也可以到达.

证明: 假设S_j不能到达可接受环, 而S_k能到达, 而 $S_k \subseteq S_j$ 代表自动机中各个进程所处节点一样, 仅仅时间约束不同, 如图2, S_j如果不能到达可接受环, 那么S_k肯定不能, 与条件矛盾.

引理2. 在状态空间中如果有 $S_k \subseteq S_j$ , 并且S_k到S_j之间包含一个接受状态, 那么S_k可以到达接受环.

证明: 状态S_j是状态S_k的超集, 而状态S_k能到达S_j, 由DBM表示的时间约束是凸性的, 可以将S_j分为S_k和S_j–S_k两部分, 故可得发现环.

由引理1还可以得出以下结论, 在状态空间中如果有 $S_j \subseteq S_k$ , 并且S_k不可以到达接受环, 那么S_j也不可以到达. 这个结论有助于避免不必要的状态展开, 由引理1逆否命题可得.

3 多核模型检测工具的实现与优化 3.1 算法简介

文献[10]中提出了一种基于Tarjan^[17]和Dijkstra^[18]算法而形成的多核并行空性检测算法, 并且实现在SPOT库中, 这个算法的主要思路如下: 采用共享的终止条件stop和一个并查集结构使得多个线程可以共享状态遍历结果, 而状态展开过程就是一个深度优先遍历过程, 在这个过程中的每一步会首先找出状态节点是处在未遍历状态、已经遍历或者已经遍历完全的状态. 从初始状态开始, 把遍历序号依次赋值给展开状态, 其中当前图的所有状态的序号都不为0. 如果当前状态的所有后继都已经被遍历过, 并且仍然不满足接受条件, 则说明该状态和其后续状态不在接受路径中, 将它们的遍历序号赋值为0, 表示已经从当前图中删除, 放入被删除状态中. 在找到一条接受路径或者完全展开全部状态后停止. 算法伪代码如图3和图4.

在算法展开状态过程中假设S表示状态节点, 有迁移S₀→S₁, 则S₁是当前遍历到的状态节点, 有如下可能:

(1) S₁没有遍历, 返回UNKNOWN(表示未遍历), 将其放入深度优先栈dfs中, 同时加入hash表中, 其中dfs表示存储遍历过程中状态的栈, 其每个元素由<当前状态, 当前迁移的接收条件, 标识符, 当前状态未遍历的后继>这样的四元组构成, hash表存储所有状态并给予唯一的标识符, Dead表示删除状态集合, 即已遍历完全无法满足接受条件的状态集合, Livenum存储活着的（不属于Dead集合的）状态.

(2) S₁出现在了Livenum表中, 即出现在当前图, 说明发现了环, 这样我们需要判断该环是否满足接受条件, 如果满足则赋值stop=1, 标记终止符为1表示结束算法, 当前线程直接返回, 其它线程收到stop=1, 也立即返回, 表示找到了路径, 性质不满足.

(3) S₁出现在Dead中, 即S₁的所有后继已经遍历, 不会出现满足条件的接受环, 那么直接跳过.

3.2 算法优化

基于此我们采取了相应的改进措施, 通过文献[3]应用于LTSmin多线程算法的改进, 我们将其应用到了我们算法上, 主要改进思路有以下两点:

如果有迁移S₁→S₂, 如果Get_status(S₂)返回UNKNOWN, 我们增加以下判断:

(1) 如果S₂是已遍历而且非死亡状态中的状态的超集, 即存在S₃属于livenum, 并且S₃包含于S₂, 则我们可以将其作为发现一个环, 以此判断找到了环, 进行是否包含接受条件的判断.

(2) 如果S₂是Dead状态的子集, 直接由引理1得, S₂后继肯定不会出现环, 可以直接跳过.

基于这两点, 我们对算法进行了相应的改动, 改动伪代码如图5, 算法及优化全部实现在CTAV工具中, 我们对结果进行了对比研究, 主要基于展开状态的变化, 如表1结果显示, 在部分模型取得了不错的效果.

3.3 算法效果比较

在多线程算法中, 单一算法在发现环的过程中往往在某一方面表现十分优秀, 而在某些例子也存在极差的表现, 在工具实现过程中基于Tarjan、Dijkstra算法, 我们比较了这两种多核算法的区别, Tarjan算法主要表现在每发现环的时候只pop最后的边, 而Dijkstra算法在发现环的时候将当前图除根节点全部pop, 这会直接导致发现接受图的效率问题, 为此, 我们采取了混合算法, 让一部分线程跑Tarjan, 一部分线程跑Dijkstra, 在实验中, 我们通过给线程加上整数标识, 让奇数线程运行Dijkstra算法, 偶数线程运行Tarjan算法. 最终表现结果如表2, 在结果中我们发现混合算法表现良好, 在各种模型下能取得相对于单一算法更佳的时间效率效果.

4 实验研究

最终我们完成了多核模型检测工具的开发和优化, 如表3显示train-gate模型下性质“[](“trans(0).Appr”→<>(“trains(0).Cross”))”为例线程数量和模型复杂化后时间效率的提升变化, 表中“原”代表原单核工具, 后续数字表示新工具采取的线程数量. 实验效果显示多核模型检测工具的效果提升是显著的, 基本与线程数量成线性相关, 当然由于机器核数的影响, 在达到峰值即机器支持的线程核数后有所下降.

同时, 我们对比了divine工具和我们工具在4线程下的时间效率, 在部分模型中取得了更好的效果, 如表4.

5 结束语

通过采用基于Tarjan和dijkstra的多线程并行的模型检测算法, 我们提高了CTAV工具对CPU的利用率, 以此提高了CTAV工具的时间效率, 同时通过符号化状态的包含关系我们提出了多核算法下的优化方案, 对状态空间的约减有一定的优化作用, 同时在CTAV工具下对比了多种多核空性检测算法的效率, 并采取混合多线程算法完成了工具的开发. 当然, 多核模型检测工具的优化仍然需要进一步的研究, 简单的利用符号化状态的包含关系约减的优化效果并不明显, 进一步的优化也是我们下一步的工作. 同时, 最新的研究中也产生了很多采取分布式资源对系统进行模型检测的研究, 如文献[19]提出采用分布式资源对发布订阅结构系统进行模型检测. 对于如何利用分布式系统进一步提高工具的效率也是我们下一步的研究方向.