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

郝宗寅 等:Petri 网的反向展开及其在程序数据竞争检测的应用 1627

本节对比了启发式反向展开与 directed unfolding 在 Petri 网可覆盖性上的效率.结果表明:415 组测试数据
中,反向展开的规模在 85 组数据上优于正向展开,在 26 组数据上与正向展开持平.实验验证了反向展开在部分
用例上的有效性,在 Petri 网的正向分支较多时,反向展开可以从目标标识出发,仅刻画与可覆盖性判定相关的系
统状态,从而提升目标标识可覆盖性判定的效率.然而,目前反向展开在多数用例中仍效率低下,主要原因分为
以下两个方面:一是冗余扩展的数量,冗余扩展数量过多会导致算法运行缓慢,且不利于启发式技术做出正确的
选择;二是由算法的特性决定的,在 Petri 网的反向分支较多时,反向展开的效率往往低于正向展开.不过,启发式
技术往往能够弥补算法在性质上的不足.因此,针对反向展开低效或失效的情况,应考虑设计更有效的启发式技
术加以优化.

5 总结与展望

本文针对安全 Petri 网的可覆盖性判定问题,提出了一种目标导向的反向展开算法.反向展开从需要做出可
覆盖性判定的目标标识出发,仅刻画与可覆盖性判定相关的系统状态,并结合 block,hmax,hsum 等启发式技术缩
减展开的规模,以此提高目标标识可覆盖判定的效率.进而,将反向展开算法应用于并发程序的形式化验证,将
并发程序的数据竞争检测问题转换为 Petri 网特定标识的可覆盖性判定问题.实验对比了启发式反向展开与
directed unfolding 在 Petri 网可覆盖性上的效率,验证了反向展开在 Petri 网的正向分支较多时可提高可覆盖性
判定效率.
然而,本文尚有很多不足.在算法效率上,一方面需要进一步减少冗余扩展的数量,并设计更加高效的启发
式技术;另一方面,可以尝试将正向展开与反向展开相结合,综合二者的优势.在数据竞争检测上,可以考虑使用
其他静态检测算法初步确定可能发生数据竞争的语句位置,在此基础上,再结合反向展开算法进行验证.此外,
文献[32]中基于展开技术探讨一般化的并发系统的健壮性、兼容性与死锁检测等问题,后续拟围绕反向展开技
术在这些领域的应用展开研究.

References:
[1] Han L, Xing K, Chen X, Xiong F. A Petri net-based particle swarm optimization approach for scheduling deadlock-prone flexible
manufacturing systems. Journal of Intelligent Manufacturing, 2018,29(5):1083−1096. https://doi.org/10.1007/s10845-015-1161-2
[2] Hu L, Liu Z, Hu W, Wang Y, Tan J, Wu F. Petri-Net-Based dynamic scheduling of flexible manufacturing system via deep
reinforcement learning with graph convolutional network. Journal of Manufacturing Systems, 2020,55:1−4. https://doi.org/10.1016/
j.jmsy.2020.02.004
[3] Fauzan AC, Sarno R, Yaqin MA. Performance measurement based on coloured Petri net simulation of scalable business processes.
In: Proc. of the 2017 4th Int’l Conf. on Electrical Engineering, Computer Science and Informatics (EECSI). IEEE, 2017. 1−6.
https://doi.org/10.1109/EECSI.2017.8239121
[4] Liu C, Zeng Q, Duan H, Wang L, Tan J, Ren C, Yu W. Petri net based data-flow error detection and correction strategy for business
processes. IEEE Access, 2020,8:43265−43276. https://doi.org/10.1109/ACCESS.2020.2976124
[5] Lu F, Tao R, Du Y, Zeng Q, Bao Y. Deadlock detection-oriented unfolding of unbounded Petri nets. Information Sciences, 2019,
497:1−22. https://doi.org/10.1016/j.ins.2019.05.021
[6] Xiang D, Liu G, Yan C, Jiang C. Detecting data inconsistency based on the unfolding technique of petri nets. IEEE Trans. on
Industrial Informatics, 2017,13(6):2995−3005. https://doi.org/10.1109/TII.2017.2698640
[7] McMillan KL. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Proc. of the
Int’l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 1992. 164−177.
[8] Engelfriet J. Branching processes of Petri nets. Acta Informatica, 1991,28(6):575−591. https://doi.org/10.1007/BF01463946
[9] Esparza J, Römer S, Vogler W. An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design, 2002,
20(3):285−310. https://doi.org/10.1023/A:1014746130920
[10] Khomenko V, Koutny M, Vogler W. Canonical prefixes of Petri net unfoldings. Acta Informatica, 2003,40(2):95−118. https://doi.
org/10.1007/s00236-003-0122-y
[11] Heljanko K, Khomenko V, Koutny M. Parallelisation of the Petri net unfolding algorithm. In: Proc. of the Int’l Conf. on Tools and
Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2002. 371−385. https://doi.org/10.
1007/3-540-46002-0_26