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

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

[12] Benito FC, Kunzle LA. Unfolding for time Petri net. IEEE Latin America Transactions, 2017,15(5):1001−1008. https://doi.org/10.
1109/TLA.2017.7912599
[13] Schwarick M, Rohr C, Liu F, Assaf G, Chodak J, Heiner M. Efficient unfolding of coloured Petri nets using interval decision
diagrams. In: Proc. of the Int’l Conf. on Applications and Theory of Petri Nets and Concurrency. Cham: Springer-Verlag, 2020.
324−344. https://doi.org/10.1007/978-3-030-51831-8_16
[14] Dong L, Liu G, Xiang D. Verifying CTL with unfoldings of Petri nets. In: Proc. of the Int’l Conf. on Algorithms and Architectures
for Parallel Processing. Cham: Springer-Verlag, 2018. 47−61. https://doi.org/10.1007/978-3-030-05063-4_5
[15] Liu G, Reisig W, Jiang C, Zhou M. A branching-process-based method to check soundness of workflow systems. IEEE Access,
2016,4:4104−4118. https://doi.org/10.1109/ACCESS.2016.2597061
[16] Chatain T, Paulevé L. Goal-Driven unfolding of Petri nets. arXiv preprint arXiv:1611.01296, 2016.
[17] Bonet B, Haslum P, Hickmott S, Thiébaux S. Directed unfolding of Petri nets. In: Proc. of the Trans. on Petri Nets and Other
Models of Concurrency I. Berlin, Heidelberg: Springer-Verlag, 2008. 172−198. https://doi.org/10.1007/978-3-540-89287-8_11
[18] Bonet B, Haslum P, Khomenko V, Thiébaux S, Vogler W. Recent advances in unfolding technique. Theoretical Computer Science,
2014,551:84−101. https://doi.org/10.1016/j.tcs.2014.07.003
[19] Abdulla PA, Iyer SP, Nylén A. SAT-Solving the coverability problem for Petri nets. Formal Methods in System Design, 2004,24(1):
25−43. https://doi.org/10.1023/B:FORM.0000004786.30007.f8
[20] Leveson NG, Turner CS. An investigation of the Therac-25 accidents. Computer, 1993,26(7):18−41. https://doi.org/10.1109/MC.
1993.274940
[21] Poulsen K. Software bug contributed to blackout. Security Focus. 2004. http://www.securityfocus.com/news/8016
[22] Joab J. Nasdaq’s Facebook glitch came from ‘race conditions’. 2012. http://www.computerworld.com/s/article/9227350
[23] Blackshear S, Gorogiannis N, O’Hearn PW, Sergey I. RacerD: Compositional static race detection. Proc. of the ACM on
Programming Languages, 2018.2(OOPSLA):1−28. https://doi.org/10.1145/3276514
[24] Chatarasi P, Shirako J, Kong M, Sarkar V. An extended polyhedral model for SPMD programs and its use in static data race
detection. In: Proc. of the Int’l Workshop on Languages and Compilers for Parallel Computing. Cham: Springer-Verlag, 2016.
106−120. https://doi.org/10.1007/978-3-319-52709-3_10
[25] Bora U, Das S, Kukreja P, Joshi S, Upadrasta R, Rajopadhye S. Llov: A fast static data-race checker for OpenMP programs. ACM
Trans. on Architecture and Code Optimization (TACO), 2020,17(4):1−26. https://doi.org/10.1145/3418597
[26] Wilcox JR, Flanagan C, Freund SN. VerifiedFT: A verified, high-performance precise dynamic race detector. In: Proc. of the 23rd
ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming. 2018. 354−367. https://doi.org/10.1145/3178487.
3178514
[27] Gu Y, Mellor-Crummey J. Dynamic data race detection for OpenMP programs. In: Proc. of the SC18: Int’l Conf. for High
Performance Computing, Networking, Storage and Analysis. IEEE, 2018. 767−778. https://doi.org/10.1109/SC.2018.00064
[28] Lidbury C, Donaldson AF. Dynamic race detection for C++ 11. ACM SIGPLAN Notices, 2017,52(1):443−457. https://doi.org/10.
1145/3093333.3009857
[29] Kavi KM, Moshtaghi A, Chen DJ. Modeling multithreaded applications using Petri nets. Int’l Journal of Parallel Programming,
2002,30(5):353−371. https://doi.org/10.1023/A:1019917329895
[30] Vallée-Rai R, Co P, Gagnon E, Hendren L, Lam P, Sundaresan V. Soot: A Java bytecode optimization framework. In: Proc. of the
CASCON 1st Decade High Impact Papers. 2010. 214−224. https://doi.org/10.1145/1925805.1925818
[31] https://github.com/Zongyin-Hao/Coverability
[32] Liu GJ. Meta-unfolding of Petri Nets: A Model Checking Method of Concurrent Systems. Beijing: Science Press, 2020 (in
Chinese).

附中文参考文献:
[32] 刘关俊.Petri 网的元展:一种并发系统模型检测方法.北京:科学出版社,2020.

附录 A

首先给出 adequate order 的定义.偏序关系≺是一个 adequate order,如果它满足:
(1) ≺是良基的;
(2) ≺是⊂的精炼,Cfg 1 ⊂Cfg 2 意味着 Cfg 1 ≺Cfg 2 ;
(3) 若 Mark(Cfg 1 )≤Mark(Cfg 2 ),Cfg 1 ≺Cfg 2 ,则对 Cfg 2 的任意前缀 E 2 ,有 E 1 满足:
Mark(Cfg 1 ⊕E 1 )≤Mark(Cfg 2 ⊕E 2 ),且 Cfg 1 ⊕E 1 ≺Cfg 2 ⊕E 2 .