Verification Method of Asynchronously Communicating Programs Based on Basic Parallel Processes

被引：0
|
作者：
Zhao Y. [1 ]
Tan J.-H. [1 ]
Li G.-Q. [1 ]
机构：
[1] School of Software, Shanghai Jiao Tong University, Shanghai
来源：
Ruan Jian Xue Bao/Journal of Software | 2022年 / 33卷 / 08期
关键词：
actor communicating system; asynchronously communicating program; basic parallel processes; model checking; reachability;
D O I：
10.13328/j.cnki.jos.006598
中图分类号：
学科分类号：
摘要：
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. © 2022 Chinese Academy of Sciences. All rights reserved.
引用
收藏
页码：2782 / 2796
页数：14
相关论文
共 27 条
  • [1] Armstrong J., Erlang, CACM, 53, 9, (2010)
  • [2] D'Osualdo E, Kochems J, Ong CHL., Automatic verification of erlang-style concurrency, Proc. of the Int’l Static Analysis Symp, pp. 454-476, (2013)
  • [3] Carlsson R., An introduction to Core Erlang, Proc. of the PLI 2001 Erlang Workshop, (2001)
  • [4] Kochems J., Verification of asynchronous concurrency and the shaped stack constraint, (2014)
  • [5] Ong CHL, Ramsay SJ., Verifying higher-order functional programs with pattern-matching algebraic data types, Proc. of the POPL, pp. 587-598, (2011)
  • [6] Sen K, Viswanathan M., Model checking multithreaded programs with asynchronous atomic methods, Lecture Notes in Computer Science: Computer Aided Verification, CAV 2006, pp. 300-314, (2006)
  • [7] Emmi M, Ganty P, Majumdar R, Et al., Analysis of asynchronous programs with event-based synchronization, Proc. of the 24th European Symp. on Programming, LNCS: Programming Languages and Systems, ESOP 2015, pp. 535-559, (2015)
  • [8] Qadeer S, Rehof J., Context-bounded model checking of concurrent software, Lecture Notes in Computer Science: Tools and Algorithms for the Construction and Analysis of Systems, the 11th Int’l Conf. (TACAS), pp. 93-107, (2005)
  • [9] Kochems J, Ong CL., Safety verification of asynchronous pushdown systems with shaped stacks, Proc. of the CONCUR 2013, 8052, pp. 288-302, (2013)
  • [10] Leroux J, Schmitz S., Reachability in vector addition systems is primitive recursive in fixed dimension, Proc. of the 34th Annual ACM/IEEE Symp. on Logic in Computer Science, LICS 2019, pp. 1-13, (2019)
123