微信服务号

微信订阅号

2025-5-11- 18
Home > Archive>Volume 34, Issue 8, 2023 >3674-3685. DOI:10.13328/j.cnki.jos.006615
PDF HTML XML Export Cite reminder
Model and Method for Verifying Asynchronous Program Based on Communication-free Petri Net
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference [20]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Asynchronous programs utilize asynchronous non-blocking calls to achieve program concurrency, and they are widely applied in parallel and distributed systems. However, it is very complex to verify asynchronous programs, and the difficulty can be ranked as EXPSPACE in terms of both safety and liveness. This study proposes a program model of asynchronous programs and defines two problems of asynchronous programs, namely, ∈-equivalence and ∈-reachability. In addition, the two problems can be proved to be NP-complete by reducing the 3-CNF-SAT to the problems and making them further reduced to the reachability of the communication-free Petri net. The case shows that the two problems can solve the verification problems of asynchronous programs.

    Reference
    [1] Ramalingam G. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Transactions on Programming Languages and Systems, 2000, 22(2): 416–430. [doi: 10.1145/349214.349241]
    [2] Leroux J, Praveen M, Sutre G. Hyper-ackermannian bounds for pushdown vector addition systems. In: Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS). Vienna: ACM, 2014. 1–10.
    [3] Leroux J, Sutre G, Totzke P. On the coverability problem for pushdown vector addition systems in one dimension. In: Proc. of the 42nd Int’l Colloquium on Automata, Languages, and Programming. Kyoto: Springer, 2015. 324–336.
    [4] D’Osualdo E, Kochems J, Ong CHL. Automatic verification of Erlang-style concurrency. In: Proc. of the 20th Int’l Static Analysis Symp. Seattle: Springer, 2013. 454–476.
    [5] Sen K, Viswanathan M. Model checking multithreaded programs with asynchronous atomic methods. In: Proc. of the 18th Int’l Conf. on Computer Aided Verification. Seattle: Springer, 2006. 300–314.
    [6] Petri CA. Kommunikation mit automaten [Ph.D. Thesis]. Bonn: University of Bonn, 1962.
    [7] Ganty P, Majumdar R. Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems, 2012, 34(1): 6. [doi: 10.1145/2160910.2160915]
    [8] Atig MF, Bouajjani A, Kumar KN, Saivasan P. Verification of asynchronous programs with nested locks. In: Proc. of the 37th IARCS Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Dagstuhl: Schloss Dagstuhl-Leibniz-Zentrum Fuer Informatik, 2018. 11.
    [9] Emmi M, Ganty P, Majumdar R, Rosa-Velardo F. Analysis of asynchronous programs with event-based synchronization. In: Proc. of the 24th European Symp. on Programming Languages and Systems. London: Springer, 2015. 535–559.
    [10] Lakos C. The consistent use of names and polymorphism in the definition of object Petri nets. In: Proc. of the 17th Int’l Conf. on Application and Theory of Petri Nets. Osaka: Springer, 1996. 380–399.
    [11] Valk R. Petri nets as token objects. In: Proc. of the 19th Int’l Conf. on Application and Theory of Petri Nets. Lisbon: Springer, 1998. 1–24.
    [12] Christensen S, Hansen ND. Coloured Petri nets extended with channels for synchronous communication. In: Proc. of the 15th Int’l Conf. on Application and Theory of Petri Nets. Zaragoza: Springer, 1994. 159–178.
    [13] Czerwiński W, Fröschle S, Lasota S. Partially-commutative context-free processes. In: Proc. of the 20th Int’l Conf. on Concurrency Theory. Bologna: Springer, 2009. 259–273.
    [14] 杨启哲, 李国强. 基于通信Petri网的异步通信程序验证模型. 软件学报, 2017, 28(4): 804-818. http://www.jos.org.cn/1000-9825/5191.htm
    Yang QZ, Li GQ. Model on asynchronous communication program verification based on communicating Petri nets. Ruan Jian Xue Bao/Journal of Software, 2017, 28(4): 804-818 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5191.htm
    [15] Esparza J. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 1997, 31(1): 13–25. [doi: 10.3233/FI-1997-3112]
    [16] Huynh DT. Commutative grammars: The complexity of uniform word problems. Information and Control, 1983, 57(1): 21–39. [doi: 10.1016/S0019-9958(83)80022-9]
    [17] Esparza J, Ganty P, Kiefer S, Luttenberger M. Parikh's theorem: A simple and direct automaton construction. Information Processing Letters, 2011, 111(12): 614–619. [doi: 10.1016/j.ipl.2011.03.019]
    [18] 丁如江, 李国强. 非交互式Petri网可覆盖性验证的高效实现. 软件学报, 2019, 30(7): 1939–1952. http://www.jos.org.cn/1000-9825/5750.htm
    Ding RJ, Li GQ. Efficient implementation of coverability verification on communication-free Petri net. Ruan Jian Xue Bao/Journal of Software, 2019, 30(7): 1939–1952 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5750.htm
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

吴志文,李国强.基于非交互式Petri网的异步程序验证模型和方法.软件学报,2023,34(8):3674-3685

Copy
Share
Article Metrics
  • Abstract:924
  • PDF: 2679
  • HTML: 1235
  • Cited by: 0
History
  • Received:September 03,2021
  • Revised:October 14,2021
  • Online: March 24,2022
  • Published: August 06,2023
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2043811Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063