基于基本并行进程的异步通信程序的验证方法
作者:
作者简介:

赵樱(1998-),女,硕士生,主要研究领域为形式化验证,程序分析与验证;
李国强(1979-),男,博士,副教授,CCF高级会员,主要研究领域为形式化方法,程序语言理论;
谭锦豪(1996-),男,博士生,主要研究领域为程序语言理论.

通讯作者:

李国强,E-mail:li.g@sjtu.edu.cn

中图分类号:

TP311

基金项目:

国家自然科学基金(61872232,61732013)


Verification Method of Asynchronously Communicating Programs Based on Basic Parallel Processes
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [32]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    异步通信程序是进程间通过异步消息通信实现非阻塞并发的程序.当前异步通信程序的程序验证问题通常将其归约至向量加法系统及其扩展模型,因而复杂度很高,缺乏高效工具.基本并行进程作为向量加法系统的一个子类,其可达性的验证问题为NP完备.首先,改进了Osualdo等人提出的为异步通信程序建模的Actor通信系统,将其归约至基本并行进程.然后,实现了基本并行进程的模型检测工具RABLE,实验结果表明,验证方法在异步通信程序的一系列程序验证问题上具有比已有工具更高效的结果.

    Abstract:

    Asynchronously communicating program is the program that processes achieve non-blocking concurrency through asynchronous message passing. At present, the verification problem of asynchronously communicating program is usually reduced to vector addition system and its extension model, so it has high complexity and lack of efficient tools. Basic Parallel Processes, as a subclass of vector addition system, whose verification of complexity reachability is NP-complete, can also be used as an important model for verifying concurrent programs. Firstly, improve the Actor communicating system proposed by Osualdo, et al., by reducing it to Basic Parallel Processes. Then, realizing an automatic model checker for basic parallel processes named RABLE. The experimental results show that the verification method is more efficient than the existing tools for a series of program verification problems of asynchronously communicating programs.

    参考文献
    [1] Armstrong J.Erlang.CACM, 2010, 53(9):68-75.[doi:10.1145/1810891.1810910]
    [2] D'Osualdo E, Kochems J, Ong CHL.Automatic verification of erlang-style concurrency.In:Proc.of the Int'l Static Analysis Symp.Berlin:Springer-Verlag, 2013.454-476.
    [3] Carlsson R.An introduction to Core Erlang.In:Proc.of the PLI 2001 Erlang Workshop.2001.
    [4] Kochems J.Verification of asynchronous concurrency and the shaped stack constraint.Oxford:Oxford University, 2014.
    [5] Ong CHL, Ramsay SJ.Verifying higher-order functional programs with pattern-matching algebraic data types.In:Proc.of the POPL.2011.587-598.
    [6] Sen K, Viswanathan M.Model checking multithreaded programs with asynchronous atomic methods.In:Ball T, Jones RB, eds.Lecture Notes in Computer Science:Computer Aided Verification, CAV 2006.Seattle:Springer-Verlag, 2006.300-314.[doi:10.1007/11817963_29]
    [7] Emmi M, Ganty P, Majumdar R, et al.Analysis of asynchronous programs with event-based synchronization.In:Vitek J, ed.Proc.of the 24th European Symp.on Programming, LNCS:Programming Languages and Systems, ESOP 2015.London:Springer-Verlag, 2015.535-559.
    [8] Qadeer S, Rehof J.Context-bounded model checking of concurrent software.In:Halbwachs N, Zuck LD, eds.Lecture Notes in Computer Science:Tools and Algorithms for the Construction and Analysis of Systems, the 11th Int'l Conf.(TACAS).Berlin:Springer-Verlag, 2005.93-107.
    [9] Kochems J, Ong CL.Safety verification of asynchronous pushdown systems with shaped stacks.In:D'Argenio PR, Melgratti HC, eds.Proc.of the CONCUR 2013, Vol.8052.Berlin:Springer-Verlag, 2013.288-302.
    [10] Leroux J, Schmitz S.Reachability in vector addition systems is primitive recursive in fixed dimension.In:Proc.of the 34th Annual ACM/IEEE Symp.on Logic in Computer Science, LICS 2019.Vancouver:IEEE, 2019.1-13.[doi:10.1109/LICS.2019.8785796]
    [11] Czerwinski W, Lasota S, Lazic R, et al.The reachability problem for Petri nets is not elementar.In:Charikar M, Cohen E, eds.Proc.of the 51st Annual ACM SIGACT Symp.on Theory of Computing, STOC 2019.New York:ACM, 2019.24-33.[doi:10.1145/3313276.3316369]
    [12] Rackoff C.The covering and boundedness problems for vector addition systems.Theoretical Computer Science 6, 1978, 223-231.
    [13] Esparza J.Decidability and complexity of Petri net problems-An introduction.In:Advanced Course on Petri Nets.Berlin:Springer-Verlag, 1996.374-428.[doi:10.1007/3-540-65306-6_20]
    [14] Kaiser A, Kroening D, Wahl T.Efficient coverability analysis by proof minimization.In:Koutny M, Ulidowski I, eds.Proc.of the CONCUR 2012.LNCS 7454, Berlin:Springer-Verlag, 2012.500-515.[doi:10.1007/978-3-642-32940-1_35]
    [15] Esparza J, Ledesma-Garza R, Majumdar R, et al.An SMT-based approach to coverability analysis.In:Biere A, Bloem R, eds.Proc.of the CAV 2014.Cham:Springer-Verlag, 2014.603-619.
    [16] Christensen S.Decidability and decomposition in process algebras[Ph.D.Thesis].Edinburgh:The University of Edinburgh, Department of Computer Science, 1993.
    [17] Verma KN, Seidl H, Schwentick T.On the complexity of equational horn clauses.In:Nieuwenhuis R, ed.Proc.of the Automated Deduction-CADE2020.LNCS 3632.Berlin:Springer-Verlag, 2005.337-352.
    [18] 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 nglish abstract).http://www.jos.org.cn/1000-9825/5191.htm[doi:10.13328/j.cnki.jos.005191]
    [19] 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[doi:10.13328/j.cnki.jos.005750]
    [20] Tan JH, Li GQ.Bounded model checking liveness on basic parallel processes.Ruan Jian Xue Bao/Journal of Software, 2020, 31(8):2388-2403(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5959.htm[doi:10.13328/j.cnki.jos.005959]
    [21] Fu H.Model checking EGF on basic parallel processes.In:Proc.of the 9th Int'l Symp.on Automated Technology for Verification and Analysis.Berlin:Springer-Verlag, 2011.120-134.[doi:10.1007/978-3-642-24372-1_10]
    [22] 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]
    [23] Karp RM, Miller RE.Parallel Program Schemata.Journal of Computer and System Sciences, 1969, 3(2):147-195.
    [24] Barrett C, Tinelli C.Satisfiability modulo theories.Journal on Satisfiability Boolean Modeling and Computation, 2018, 3(3):141-224.
    [25] Moura LD, Bjørner N.Z3:An efficient SMT solver.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer-Verlag, 2008.337-340.
    [26] Tan JH.Verification of asynchronous communication program based on basic parallel processes[MS.Thesis].Shanghai:Shanghai Jiao Tong University, 2020(in Chinese with English abstract).
    [27] Hague M, Lin A W.Synchronisation-and reversal-bounded analysis of multithreaded programs with counters.In:Madhusudan P, Seshia SA, eds.Proc.of the 24th Int'l Conf.on Computer Aided Verification.LNCS 7358, Berlin:Springer-Verlag, 2012.260-276.
    附中文参考文献:
    [18] 杨启哲,李国强.基于通信Petri网的异步通信程序验证模型.软件学报, 2017, 28(4):804-818.http://www.jos.org.cn/1000-9825/5191.htm[doi:10.13328/j.cnki.jos.005191]
    [19] 丁如江,李国强.非交互式Petri网可覆盖性验证的高效实现.软件学报, 2019, 30(7):1939-1952.http.//www.jos.org.cn/1000-9825/5750.htm[doi:10.13328/j.cnki.jos.005750]
    [20] 谭锦豪,李国强.基本并行进程活性的限界模型检测.软件学报, 2020, 31(8):2388-2403.http://www.jos.org.cn/1000-9825/5959.htm[doi:10.13328/j.cnki.jos.005959]
    [26] 谭锦豪.基于基本并行进程的异步通信程序验证研究[硕士学位论文].上海:上海交通大学, 2020.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

赵樱,谭锦豪,李国强.基于基本并行进程的异步通信程序的验证方法.软件学报,2022,33(8):2782-2796

复制
分享
文章指标
  • 点击次数:1161
  • 下载次数: 4057
  • HTML阅读次数: 2581
  • 引用次数: 0
历史
  • 收稿日期:2021-09-04
  • 最后修改日期:2021-10-14
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
文章二维码
您是第19766043位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号