Page 40 - 《软件学报》2021年第6期

1614 Journal of Software 软件学报 Vol.32, No.6, June 2021

(a) 反向展开适用场景 (b) 正向展开适用场景
Fig.1 Suitable scenarios for forward unfolding and reverse unfolding
图 1 正向展开与反向展开的适用场景

从上述两个例子中可观察到:当 Petri 网的正向分支较多时,反向展开往往更加适用;当 Petri 网的反向分支
较多时,正向展开往往更加适用.具体而言,正向展开从 Petri 网的初始标识出发刻画系统,隐含了系统完整行为;
而反向展开从需要做出可覆盖性判定的目标标识出发,仅刻画与可覆盖性判定相关的系统状态.本文正是从这
个角度出发设计并实现了反向展开算法.
接下来,将结合一个实例进一步说明反向展开相比正向展开的优势.图 2(a)中,Petri 网的初始标识为{p1},需
[9]
验证目标标识{p10}的可覆盖性.图 2(b)是 Petri 网的正向展开 .图 2(c)是 Petri 网的反向展开.二者都采用基于
广度优先策略的 adequate order 作为扩展顺序,一旦验证目标标识的可覆盖性就终止扩展.在这个例子中,正向展
开共产生 19 个节点、20 条流关系,反向展开总共产生 14 个节点、14 条流关系,反向展开的规模优于正向展开.
这是因为变迁{t1,t3,t4,t7}对于{p10}可覆盖性的贡献是冗余的(即“左侧”的路径是冗余的).正向展开隐含了系
统的完整行为,难以避免对{t1,t3,t4,t7}的冗余行为分析.而反向展开仅刻画与可覆盖性判定相关的系统状态,避
免了对{t3,t7}的冗余刻画.尽管反向展开中仍有冗余,但总体规模优于正向展开.

(a) Petri 网实例 (b) Petri 网的正向展开 (c) Petri 网的反向展开
Fig.2 An example where reverse unfolding is better than forward unfolding
图 2 反向展开优于正向展开的实例
本节论述了正向展开与反向展开各自的优势.值得一提的是:这种相互之间的优势是由算法的性质决定的,
具备一定的一般性.像 goal-driven unfolding [16] ,directed unfolding [17] 等正向展开,尽管它们会使用内部因果关系