2. 计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190
2. State Key Laboratory of Computer Science(Institute of Software, The Chinese Academy of Sciences), Beijing 100190, China
互模拟[1]是并发理论[2]中最重要的概念之一, 它提供了一种有用的验证技术[3]来比较交互系统的可观察行为.如果它们能够一步步地匹配彼此的移动, 则两个系统是互模拟的.检测互模拟的算法通常可以分为两类:全局算法和局部算法[4, 5].
全局算法主要验证一个系统中任意两个状态是否互模拟(有时我们比较两个系统的初始状态, 可事先把两个系统拼接成一个更大的系统), 它需要预先生成一个整体的状态系统.相比较之下, 局部算法只需要判定给定的两个状态是否互模拟, 同时检查这两个状态可达到的后续状态的行为关系.Fernandez和Mounier[6]提出了第1种局部算法, 他们的算法通过遍历的方式动态地验证两个状态是否互模拟, 这个算法主要是一边检验等价关系一边增加要考察的状态.Du和Deng[7]提出了一种准局部算法来验证互模拟.对于一些类型的标记迁移系统(LTS), 例如简单的LTS和确定型LTS, 准局部算法具有更好的时间复杂度.然而在许多实际运用中, 我们遇到的不是简单的LTS, 因此原始的准局部算法并不适用.
本文提出了一种准局部算法的扩展算法, 使其能够适用于一般的LTS.我们在Java中实现了扩展算法, 并将其与局部算法进行比较.我们以VLTS为基准[8], 其中包含各种大小不同的LTS, 状态个数从几百到几十万.
通过实验, 我们抽取了20多个具有代表性的例子进行验证, 通过观察运行的时间来比较两种算法.在大多数的情况下, 准局部算法确实比局部算法更快.特别是处理确定型的LTS时, 准局部算法比局部算法有明显的优势.为了验证模拟关系, 我们还修改了这两种算法.我们的实验也显示了类似的现象—在大多数情况下, 准局部算法优于局部算法.
为了使实现的算法有更加广泛的应用, 我们调查了生成LTS的方法, 发现可以利用Fiarce语言通过TINA, CADP等工具生成LTS, 以及CADP提供的LOTOS语言转换为LTS.随后可以用我们实现的算法进行验证.另外, 我们利用弱互模拟的定义对LTS进行饱和处理, 再用我们实现的算法验证, 极大地丰富了算法的可适用性.
本文第1节给出一些基本的准备知识.第2节回顾典型的互模拟算法.第3节介绍扩展的准局部算法.第4节将扩展算法的时间效率与局部算法时间效率进行比较.第5节考虑弱互模拟的情况, 并提取实例进行实验计算运行时间.第6节总结本文的贡献与不足, 并阐明后续的一些工作方向.
1 准备知识我们将回顾操作模型的一些基本定义以及互模拟[1, 2]的概念.在计算机科学中, 迁移系统常常被用作描述系统行为的操作模型, 它们是一种有向图, 其中, 节点代表状态, 有向边代表迁移.
定义1. 一个标记迁移系统是一个四元组(S, s0, A, →), 其中,
● S表示有限的状态集合;
● s0∈S表示初始状态;
● A表示有限的标记集合(有时候也称为动作);
● →⊆S×A×S表示标记转移关系.
一般把(s1, a, s2)∈→写成
定义2. 一个双重标记迁移系统(DLTS)是由一个五元组组成(S, s0, L, A, →), 其中, (S, s0, A, →)是一个LTS, 并且L:S→{0, 1}是一个标号函数.
简单标记迁移系统可以表示为:对于所有的状态s, s'和标号a, b, 如果
定义3. 二元关系R⊆S×S称为互模拟关系, 如果对任意的状态对(s, t), 当s R t成立时满足以下条件.
● 若
● 若
一个由所有互模拟状态对组合成的最大的互模拟等价关系叫做互模拟等价关系.
2 互模拟验证算法给定一个LTS和两个状态s与t, 一个自然的问题是问s与t是否互模拟.Paige和Tarjan[9]设计了一种分割精化算法, 生成给定状态的所有互模拟等价关系类.所以如果s和t属于相同的等价类, 那么他们是互模拟的.这个算法是全局的, 它需要知道整个系统的状态, 包括那些无关的状态, 通过检查所有的状态以及它们的后续状态是否在同一个等价类中, 来不断地把状态集合划分.Fernandez和Mounier[6]提出了一种名为on the fly的算法, 这是一种只需要验证相关s和t的转移行为的算法.基本思想如下:在通常情况下, s和t分别是两个LTS如L1和L2的初始状态.通过深度优先搜索(DFS)遍历两个LTS的乘积, 表示为L1||L2.经过遍历, 如果复合状态s'||t'被访问但还未被分析, 我们假设s'和t'互模拟并继续进行DFS遍历.如果两个状态再遍历之后被证明是非互模拟, 则原先的假设不成立, 继而进行另一次DFS遍历.此次的遍历只能证明两个状态不是互模拟.在比较糟糕的情况下, 每经历一次DFS只能验证一对状态不是互模拟, 因此会出现很多重复的情况.为了解决这个问题, Du和Deng[7]提出了一种准局部(quasi-local)算法.
准局部算法的主要思想如下:给定两个LTS如L1和L2[6], 首先我们通过on the fly的遍历思想, 利用两个迁移系统的积构造成一个新的有向图, 如果s和t有不同的初始动作, 则我们将L1||L2中的状态s||t标记为0;反之标记为1.显然:如果s||t被标记为0, 则s和t一定不是互模拟的; 如果被标记为1, 我们暂时还不能确定状态s和t为互模拟.于是, 下一步将标记0扩散到每一个不是互模拟的状态对.扩散过程为后退行为.
例如:如果
实现算法主要用到两个数据结构.
● 一个栈St存储所有0标记的状态, 只要St不为空, 我们每次移去栈顶的元素, 然后开始一轮从它出发的0标记扩散过程.每次得到一个新的0标记的状态, 并把它压入栈St中;
● 定义一个三维数组Ar1[k, i, l], 对于转移
为了使生成的算法[7]不仅仅只适用于简单的LTS, 即:两个给定的状态, 可能存在不只一个的迁移关系, 我们将三维数组Ar1增加一维, 利用四维数组来计算, 第四维把迁移动作也考虑进去.例如, Ar1[k, i, l, a]存储对应于从sk到si的动作为a的迁移, 存在从tl出发的候选迁移的个数.Ar2也做相似的设置.然而, 对于大型的LTS而言存在上百万的状态, 使用多元数组的方式会使得程序较难执行, 并且会占用较大的空间.在执行算法时也会容易出现内存溢出.幸运的是, 我们观察到, 数组Ar1和数组Ar2在通常情况下是稀疏的, 所以可以在实现算法的时候, 利用哈希表替代四元组.哈希表会使算法执行更快、更能节约内存.
扩展后的准局部算法见算法1.
算法1. The optimized quasi-local algorithm.
1: construct the DLTS L:=S||RT and initialize Ar1 and Ar2
2: if L(s0||t0)=0 then return FALSE
3: end if
4: initialize St:=∅ and L'=L
5: perform a width first traversal of L and push a pair (i, j) into St whenever
L(si||tj)=0
6: while St:=∅ do
7: (i, j):=pop(St)
8: for all (sk||tl)∈Pred(si||tj) with L'(sk||tl)=1 do
9: decrease both Ar1[k, i, l, a] and Ar2[l, j, k, a] by 1
10: if Ar1[k, i, l, a]=0 or Ar2[l, j, k, a]=0 then
11: set L'(sk||tl)=0
12: if (k, l)=(0, 0) then
13: return FALSE
14: end if
15: push (k, l) into St
16: end if
17: end for
18: end while
19: return TRUE
修改后的算法与原先的大致相同[7], 主要区别在于前面介绍的两个四维数组和在实际实现算法过程中使用哈希表.Ar1的初始值就是迁移
用双重标记迁移系统证明互模拟等价的方法Du和Deng已经给予正确性证明.以下是修改后的算法例子验证, 由于修改后的算法, 可以验证一般的迁移系统, 于是下面给出的两个系统为一般的迁移系统(如图 1所示).
图 1(a)、图 1(b)为S和T的两个标记迁移系统, 用这两个系统构建一个DLTS系统图 1(c).因为s4可以执行动作e而t4不可以, 所以将状态(s4||t4)标记为0, 即t4不模拟s4.而状态(s2||t2)是状态(s3||t4)唯一的一个父节点, 因为系统S中
反之, 观察系统S是否模拟系统T, 以上述同样的方法构建DLTS, 调换状态s与t的位置即可, 以同样的方式标记0, 并做扩散, 最后可得状态(s0||t0)为稳定为1, 则S能模拟T.所以系统S与T不能互模拟.
扩展后的算法与扩展前的算法除了可以验证标记迁移系统之外, 还增加了系统验证的范围.前人已按照原始算法, 利用Java进行实现, 但实现的算法可验证的系统最大迁移量为10 000, 并且只做了4组实验, 这4组实验并无具体数据由来, 无法确保实验的正确性.扩展后的算法经过分析改正以及数据结构的扩展处理, 可以验证百万的迁移量(具体参见第4节); 同时, 实验数据为CADP权威发布的数据, 具有一定的可靠性.
4 算法的实现与比较令L1和L2是两个LTS, 其初始状态分别为s0和t0.局部算法和准局部算法都可以验证s0是否与t0是互摸拟的.假设系统L1(或L2)的状态个数为n1(或n2), 并用m1(或m2)表示迁移个数.最糟糕的情况下, 局部算法的时间复杂度为O(n12n22).准局部算法的时间复杂度为O(m1m2).对于简单的LTS, mi≤ni2其中, i=1, 2.准局部算法有很好的时间复杂度, 但是对于一般的LTS并不一定是如此.
除了理论分析, 我们比较两种算法的实际效率.我们已经在Java中实现算法.实验环境如下:Windows 7 professioal; Intel(R) Core(TM) i7-4790 CPU 3.60GHz; RAM: 8.00GB.
我们的实验数据以VLTS为基准[8], 这是一个标记迁移系统的集合.VLTS的基准获取是来自不同的通信协议和并发系统, 都是对应于现实工业系统中的例子.对于表 1中运用到的每个例子, 我们首先从CADP[10]中下载BCG格式的LTS, 然后运用CADP自带的分离精化方法, 使例子最小化, 从而得到一个最简化的LTS与原来的LTS是互摸拟的.CADP是为同步并发系统设计的一个很优秀的工具, 我们运用实现的两个算法来验证这两个LTS, 表 1给出经过处理的各例子运行的时间.
对于每个种算法, 我们都使用了深度优先搜索遍历(DFS)和宽度优先搜索遍历(WFS)两种方式来实现.DFS和WFS区别在于验证状态时的顺序, 并不会影响算法的正确性.对于局部算法, 我们发现DFS比WFS更加适用, 具体两者的比较见表 1.在局部算法中, DFS直接遍历要判断的两个状态的后续继状态对, 我们立即就可以得到这两个状态是否互摸拟的结果; 然而WFS并不能直接就访问后继的状态对, 而是访问兄弟节点上的状态对, 所以不能快速地得到两个状态是否互摸拟的结果.然而对于准局部算法来说, 两种搜索遍历仅仅是用来构建DLTS并不会对验证速度产生影响, 因此准局部算法的两种遍历结果时间上几乎相同; 见表 1中的第7列、第8列所示.
比较DFS实现的两个算法, 从表中的第7列、第9列可以看出, 准局部算法有明显的优势.在我们运行的22个例子中, 有17个例子(其余5个例子在表 1中标记为灰色)显示准局部算法比局部算法时间效率更为优秀.特别是对于确定型的LTS(在表 1中第2列标记为D), 准局部算法优于局部算法(见表 1第6列、第8列).我们还修改了两个算法用于检查模拟关系.具体数据可参见https://github.com/zhengxiaolin123/bisimulation.
5 弱互模拟在实际的实例中, 我们有时候会提取到两个系统并不全为强互模拟的情况, 也有弱互摸拟.为了验证的丰富性, 我们对给定的LTS进行饱和处理, 使算法也能验证弱互模拟.
定义4. 令(S, s0, A, →)为一个标记迁移系统, τ∈A为不可见迁移动作.二元关系R⊆A×A是一个弱模拟关系, 如果对于任意的状态对(s, t), 当s R t成立时满足以下条件:
● 若
● 如果
如果R和它的逆关系R-1都是弱模拟关系, 那么R是弱互模拟关系.
由定义可以观察到:为验证弱互模拟关系, 我们可以先对给定的LTS做一个饱和(saturation)处理, 然后运用前面介绍的互模拟验证算法.所谓饱和处理, 就是把原来的迁移系统(S, s0, A, →)转化为新的系统(S, s0, A, ⇒), 其中, ⇒的定义如下:
● 如果a≠τ, 那么
●
即:我们利用Java程序将不可见迁移动作τ进行处理, 将迁移状态
我们通过以上定义对获取到的LTS进行饱和处理, 随即运用于两个算法之中进行互模拟检测.为了使我们实现的算法能运用于现实的例证中, 我们用提取实例生成的LTS进行实验, 表 2中备注表明了各例子名称, 具体可参照CADP.这些实例都由CADP提供的工具进行处理, 生成LTS, 再由我们根据弱互摸拟定义对生成的LTS进行转换, 然后用于实现好的算法中验证.将实例生成LTS的方式有很多种, 比如:Firace语言就是将实际的系统装换为Fiacre语言, 并且利用Tina等工具进行转换.CADP中也提供了LOTOS等转换为LTS的方法(实验中给出的实例就是经由LOTOS转换生成).将转换好的LTS进行饱和处理, 就可运用于我们所实现的算法之中.表 2也给出了CADP处理互摸拟的时间效率, CADP采用的编写方式为C语言, 它用于处理弱互摸拟还是比较有优势的.
我们以比特交换协议(alternating bit protocol, 简称ABP)为例子[17], 比特交换协议是在数据链路层上运行的一个简单的网络协议, 它使用FIFO语义传输丢失或损坏的消息.分析ABP说明规范, 将其转换为LOTOS语言. CADP在Demo_Example的demo2里面已经给出了ABP说明规范转换为LOTOS语言, 我们利用CADP工具提取LOTOS文件并将它利用CAESAR转换成LTS, 即bcg格式, 再将bcg格式提取出来转化为txt格式.我们再将txt进行饱和处理, 去除不可见的状态, 这是因为我们具体实现的ABP是一个不含有不可见状态的LTS.处理好的LTS为1 161个状态、456个迁移量、10个迁移动作.
Fiacre是一种用于实时系统的高级描述语言, 它能将程序转换LTS, 我们利用Fiacre实现ABP, .参考Fiacre网站提供的ABP实现方法[19].
abp.fcr
1: type seqno is bool
2: type packet is seqno
3: process buffer
4: [ii: in packet, oo: out packet]
5: is
6: states idle
7: var buff: queue 1 of packet:={||},
8: pkt: packet
9: from idle
10: select
11: ii? pkt;
12: on not (full buff);
13: buff:=enqueue(buff, pkt);
14: to idle
15: []
16: on not (empty buff);
17: oo! first buff;
18: buff:=dequeue buff;
19: to idle
20: []
21: wait [0, 1];
22: on not (empty buff);
23: buff:=dequeue buff;
24: # lost;
25: to idle
26: end
27: process sender
28: [mbuff: out packet, abuff: in packet
29: is
30: states idle, send, waita
31: var ssn, n: seqno:=false
32: from idle
33: to waita
34: from send
35: mbuff! ssn;
36: to waita
37: from waita
38: select
39: abuff? n;
40: if n=ssn then
41: ssn:=not ssn
42: end;
43: to idle
44: []
45: wait [4,5];
46: to send
47: end
48: process receiver
49: [mbuff: in packet, abuff: out packet]
50: is
51: states rcve, ack
52: var rsn: seqno:=false,
53: m: packet:=true
54: from rcve
55: mbuff? m;
56: if m=rsn then
57: rsn:=not rsn;
58: to ack
59: else
60: to ack
61: end
62: from ack
63: abuff! m;
64: to rcve
65: component abp
66: is
67: port minp: in out packet in [0, 0],
68: mout: in out packet in [0, 1],
69: ainp: in out packet in [0, 2],
70: aout: in out packet in [0, 1]
71: par * in
72: sender[minp, aout]
73: ||buffer[minp, mout]
74: ||buffer[ainp, aout]
75: ||receiver[mout, ainp]
76: End
77: abp
我们将实现好的伪代码在已安装的Fiacre, Tina环境中利用Fiacre工具, 使用语句frac abp.fcr abp.tts生成一个tts包, 这个tts包里面包含abp.c, abp.h, abp.ltl, abp.ndr, abp.det.然后, 我们利用Tina工具, 使用语句:tina—a abp.ndr abp.aut(abp.bcg)将fcr文件转换为aut文件或者bcg文件, 再利用CADP将其转换为LTS.我们以同样的方式进行处理LTS文件, 处理好的文件有61个状态、283个迁移量以及10个迁移动作.
我们将说明规范生成的LOTOS与利用Fiacre语言、根据说明规范实现的ABP.用我们已经实现的算法进行验证, 发现Fiacre生成的LTS能模拟说明规范LOTOS语言生成的LTS, 时间效率为0.016s.而ABP说明规范的LOTOS并不能模拟我们所实现的ABP, 所以两个不是互模拟关系.我们实现的互模拟算法也验证了这一点, 从而可以证明我们实现的4种算法可以用于验证两段程序是否可以模拟或者互模拟来验证实现某种规范算法的正确性.
生成LTS还有一种比较常见的方法是还包括LTSA工具来生成, 利用FSP语言编写.lts文件, 可用ABP作为例子[16]已经给出.可利用CADP生成文件形式的LTS或者利用LTSA进行图形转换.
所以只要分析系统将系统转换为相应的语言, 再将其转换为LTS, 再用实现的算法来验证是否互模拟或者模拟.现实研究中的意义在于可以验证转换器、编译器等的正确性.Julio C.Peralta等人[18]将SIGNAL转换成Fiacre语言, 并将Fiacre利用CADP转换成LTS.同时, 利用编译器将SIGNAL生成的C语言, 将C语言转换为Fiacre语句, 以同样的方法转换为LTS.比较这两个LTS为互模拟.从而验证了互模拟的编译器的正确性.
6 总结与展望我们扩展了Du和Deng的准局部算法, 使其不再只能验证简单的LTS, 还可验证一般的LTS.用Java实现准局部算法并与局部算法进行比较, 根据实验数据表明, 准局部算法比局部算法更为优秀.我们也修改了算法, 让其能验证模拟的系统.最后用于实例中测试, 并扩展处理弱互摸拟关系.我们的实验数据以VLTS为基准, 实例验证的数据由CADP提供测试用例.
近来, Groote和Wijs[11]提出了一种有效的全局算法, 用于验证分支互模拟, 重点在于辅助数据结构的使用. Wijs[12]提出了采用并行的GPU加速算法.Dalsgaard等人[13]已经发明了一种分布式算法, 计算稳定的依赖图.目前还不清楚这种相似的思想是否可以用于准局部算法.
Kundu[14]倡导了一种验证互摸拟的高级合成技术和定理证明, 以此引发了一系列的研究工作[15], 我们期待它可以用来扩展我们的准局部算法.
[1] |
Park D. Concurrency and automata on infinite sequences. In: Proc. of the GI-Conf. on Theoretical Computer Science. 1981. 167-183. [doi:10.1007/BFb0017309] |
[2] |
Milner R. Communication and Concurrency. Prentice-Hall, Inc, 1989.
|
[3] |
Sangiorgi D. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011.
|
[4] |
Dovier A, Piazza C, Policriti A. An efficient algorithm for computing bisimulation equivalence. Theoretical Computer Science, 2002, 311(1-3): 221–256.
[doi:10.1016/S0304-3975(03)00361-X] |
[5] |
Fisler K, Vardi MY. Bisimulation minimization and symbolic model checking. Formal Methods in System Design, 2002, 21(1): 39–78.
[doi:10.1023/A:1016091902809] |
[6] |
Fernandez JC, Mounier L. Verifying bisimulations on the fly. In: Proc. of the 3rd Int'l Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols. North-Holland Publishing Co., 1990. 95-110. |
[7] |
Du WJ, Deng YX. A quasi-local algorithm for checking bisimilarity. In: Proc. of the IEEE Int'l Conf. on Computer Science and Automation Engineering. 2011. 1-5. [doi:10.1109/CSAE.2011.5952411] |
[8] |
The VLTS benchmark suite. http://cadp.inria.fr/resources/vlts/ |
[9] |
Valmari A. Simple bisimilarity minimization in O(mlogn) time. Applications and Theory of Petri Nets, 2010, 105(3): 319–339.
[doi:10.3233/FI-2010-369] |
[10] |
Garavel H, Lang F, Mateescu R, Serwe W. CADP 2011:A toolbox for the construction and analysis of distributed processes. Software Tools for Technology Transfer, 2013, 15(2): 89–107.
[doi:10.1007/s10009-012-0244-z] |
[11] |
Groote JF, Wijs A. An O(mlogn)) algorithm for stuttering equivalence and branching bisimulation. In: Proc. of the 22nd Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 9636, Springer-Verlag, 2016. 607-624. [doi:10.1007/978-3-662-49674-9_40] |
[12] |
Wijs A. GPU accelerated strong and branching bisimilarity checking. In: Proc. of the 21st Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 9035, Springer-Verlag, 2015. 368-383. [doi:10.1007/978-3-662-46681-0_29] |
[13] |
Dalsgaard AE, Enevoldsen S, Larsen KG, Srba J. Distributed computation of fixed points on dependency graphs. In: Proc. of the 2nd Int'l Symp. on Dependable Software Engineering: Theories, Tools, and Applications. LNCS 9984, Springer-Verlag, 2016. 197-212. [doi:10.1007/978-3-319-47677-3_13] |
[14] |
Kundu S, Lerner S, Gupta R. Validating high-level synthesis. In: Proc. of the 20th Int'l Conf. on Computer Aided Verification. LNCS 5123, Springer-Verlag, 2008. 459-472. [doi:10.1007/978-3-540-70545-1_44] |
[15] |
Hao KC, Ray S, Xie F. Equivalence checking for function pipelining in behavioral synthesis. In: Proc. of the DATE 2014. European Design and Automation Association, 2014. 1-6. [doi:10.7873/DATE.2014.163] |
[16] |
http://www.doc.ic.ac.uk/~jnm/LTSdocumention/AB_example.html |
[17] |
Wikipedia. https://en.wikipedia.org/wiki/Alternating_bit_protocol |
[18] |
Peralta JC, Gautier T, Besnard L, Guernic PL. LTS for Translation Validation of (multi-clocked) SIGNAL Specifications. IEEE, 2010.
[doi:10.1109/MEMCOD.2010.5558632] |
[19] |
Fiacre. http://projects.laas.fr/fiacre/ |