微信服务号

微信订阅号

2025-4-3- 19
Home > Archive>Volume 28, Issue 4, 2017 >804-818. DOI:10.13328/j.cnki.jos.005191
PDF HTML XML Export Cite reminder
Model on Asynchronous Communication Program Verification Based on Communicating Petri Nets
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61672340, 61472238, 91318301)

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

    Since multi-stack models are generally Turing-complete, verification problems on general models for asynchronous communication programs are undecidable. This paper proposes a new model based Petri net, named communication Petri nets (C-Petri nets) to model asynchronous communication programs. Applying the k-shaped restriction on the input communications and the abstraction on each stack based on popping lemma of regular languages, the coverability problem of the restricted C-Petri net is decidable by encoding the model to data Petri nets.

    Reference
    [1] Ramalingam G. Context-Sensitive synchronization-sensitive analysis is undecidable. ACM Trans. on Programming Languages and Systems (TOPLAS), 2000,22(2):416-430.[doi:10.1145/349214.349241]
    [2] Sen K, Viswanathan M. Model checking multithreaded programs with asynchronous atomic methods. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2006. 300-314.[doi:10.1007/11817963_29]
    [3] Kochems J, Ong CHL. Safety verification of asynchronous pushdown systems with shaped stacks. In:Proc. of the Int'l Conf. on Concurrency Theory. Berlin, Heidelberg:Springer-Verlag, 2013. 288-302.[doi:10.1007/978-3-642-40184-8_21]
    [4] Petri CA. Kommunikation mit automaten[Ph.D. Thesis]. University of Bonn, 1962.
    [5] Lazić R, Newcomb T, Ouaknine J, Roscoe AW, Worrell J. Nets with tokens which carry data. Fundamenta Informaticae, 2008, 88(3):251-274.
    [6] Emmi M, Ganty P, Majumdar R, Rosa-Velardo F. Analysis of asynchronous programs with event-based synchronization. In:Proc. of the European Symp. on Programming Languages and Systems. Berlin, Heidelberg:Springer-Verlag, 2015. 535-559.[doi:10. 1007/978-3-662-46669-8_22]
    [7] D'Osualdo E, Kochems J, Ong CHL. Automatic verification of Erlang-style concurrency. In:Proc. of the Int'l Static Analysis Symp. Berlin, Heidelberg:Springer-Verlag, 2013. 454-476.[doi:10.1007/978-3-642-38856-9_24]
    [8] D'Osualdo E, Kochems J, Ong L. Soter:An automatic safety verifier for Erlang. In:Proc. of the 2nd Edition on Programming Systems, Languages and Applications Based on Actors, Agents, and Decentralized Control Abstractions. ACM Press, 2012. 137-140.[doi:10.1145/2414639.2414658]
    [9] Kochems J. Verification of asynchronous concurrency and the shaped stack constraint[Ph.D. Thesis]. University of Oxford, 2015.
    [10] Cai X, Ogawa M. Well-Structured pushdown systems. In:Proc. of the Int'l Conf. on Concurrency Theory. Berlin, Heidelberg:Springer-Verlag, 2013. 121-136.[doi:10.1007/978-3-642-40184-8_10]
    [11] Jhala R, Majumdar R. Interprocedural analysis of asynchronous programs. ACM SIGPLAN Notices, 2007,42(1):339-350.[doi:10. 1145/1190215.1190266]
    [12] Ganty P, Majumdar R, Rybalchenko A. Verifying liveness for asynchronous programs. ACM SIGPLAN Notices, 2009,44(1):102-113.[doi:10.1145/1594834.1480895]
    [13] Ganty P, Majumdar R. Algorithmic verification of asynchronous programs. ACM Trans. on Programming Languages and Systems (TOPLAS), 2012,34(1):6.[doi:10.1145/2160910.2160915]
    [14] Majumdar R, Wang Z. BBS:A phase-bounded model checker for asynchronous programs. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer Int'l Publishing, 2015. 496-503.[doi:10.1007/978-3-319-21690-4_33]
    [15] Hague M. Parameterised pushdown systems with non-atomic writes. In:Proc. of the 31st Int'l Conf. on Foundations of Software Technology and Theoretical Computer Science. 2011. 457. http://arxiv.org/abs/1109.6264
    [16] Esparza J, Ganty P, Majumdar R. Parameterized verification of asynchronous shared-memory systems. In:Proc. of the 25th Int'l Conf. on Computer Aided Verification (CAV 2013), Vol.8044. Saint Petersburg:Springer-Verlag, 2013. 124.[doi:10.1007/978-3-642-39799-8_8]
    [17] Durand-Gasselin A, Esparza J, Ganty P, Majumdar R. Model checking parameterized asynchronous shared-memory systems. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer Int'l Publishing, 2015. 67-84.[doi:10.1007/978-3-319-21690-4_5]
    [18] La Torre S, Muscholl A, Walukiewicz I. Safety of parametrized asynchronous shared-memory systems is almost always decidable. In:Proc. of the 26th Int'l Conf. on Concurrency Theory. 2015. 72. http://drops.dagstuhl.de/opus/volltexte/2015/5381
    [19] 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). ACM Press, 2014. 63.[doi:10.1145/2603088.2603146]
    [20] Leroux J, Sutre G, Totzke P. On the coverability problem for pushdown vector addition systems in one dimension. In:Proc. of the Int'l Colloquium on Automata, Languages, and Programming. Berlin, Heidelberg:Springer-Verlag, 2015. 324-336.[doi:10.1007/978-3-662-47666-6_26]
    [21] Finkel A, Schnoebelen P. Well-Structured transition systems everywhere. Theoretical Computer Science, 2001,256(1):63-92.[doi:10.1016/S0304-3975(00)00102-X]
    [22] Chadha R, Viswanathan M. Decidability results for well-structured transition systems with auxiliary storage. In:Proc. of the Int'l Conf. on Concurrency Theory. Berlin, Heidelberg:Springer-Verlag, 2007. 136-150.[doi:10.1007/978-3-540-74407-8_10]
    [23] Rodríguez C. Verification Based on Unfoldings of Petri Nets with Read Arcs. École Normale Supérieure de Cachan, 2013.
    [24] Siebert M, Flochová J. Pnets-The verification tool based on Petri nets. In:Proc. of the World Congress on Engineering. 2013. 1. http://www.iaeng.org/publication/WCE2013/WCE2013_pp369-373.pdf
    [25] Esparza J, Ledesma-Garza R, Majumdar R, Meyer P, Niksic F. An SMT-based approach to coverability analysis. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer Int'l Publishing, 2014. 603-619.[doi:10.1007/978-3-319-08867-9_40]
    [26] Christensen S, Hansen ND. Coloured Petri nets extended with channels for synchronous communication. In:Proc. of the 15th Int'l Conf. on the Application and Theory of Petri Nets. LNCS 815, Zaragoza:Springer-Verlag, 1994. 159-178.[doi:10.1007/3-540-58152-9_10]
    [27] 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 the Application and Theory of Petri Nets. LNCS, Springer-Verlag, 1996. 380-399.[doi:10.1007/3-540-61363-3_21]
    [28] Valk R. Petri nets as token objects? An introduction to elementary object nets. In:Proc. of the 19th Int'l Conf. on the Application and Theory of Petri Nets. LNCS 1420, Springer-Verlag, 1998.[doi:10.1007/3-540-69108-1_1]
    [29] Lee JK, Palsberg J, Majumdar R, Hong H. Efficient may happen in parallel analysis for async-finish parallelism. In:Proc. of the Int'l Static Analysis Symp. Berlin, Heidelberg:Springer-Verlag, 2012. 5-23.[doi:10.1007/978-3-642-33125-1_4]
    [30] Gavran I, Niksic F, Kanade A, Rupak M, Viktor V. Rely/Guarantee reasoning for asynchronous programs. In:Proc. of the LIPIcs-Leibniz Int'l Proceedings in Informatics. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. 42. http://drops.dagstuhl.de/opus/volltexte/2015/5390
    [31] Deligiannis P, Donaldson AF, Ketema J, Lal A, Thomson P. Asynchronous programming, analysis and testing with state machines. ACM SIGPLAN Notices, 2015,50(6):154-164.[doi:10.1145/2813885.2737996]
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

杨启哲,李国强.基于通信Petri网的异步通信程序验证模型.软件学报,2017,28(4):804-818

Copy
Share
Article Metrics
  • Abstract:3915
  • PDF: 6734
  • HTML: 3623
  • Cited by: 0
History
  • Received:May 27,2016
  • Revised:November 26,2016
  • Online: January 24,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2032423Visitors
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