基于基本并行进程的异步通信程序的验证方法  

Verification Method of Asynchronously Communicating Programs Based on Basic Parallel Processes

作　　者：赵樱 谭锦豪 李国强[1] ZHAO Ying;TAN Jin-Hao;LI Guo-Qiang(School of Software,Shanghai Jiao Tong University,Shanghai 200240,China)

机构地区：[1]上海交通大学软件学院,上海200240

出　　处：《软件学报》2022年第8期2782-2796,共15页Journal of Software

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

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

关 键 词：异步通信程序 基本并行进程 Actor通信系统 模型检测 可达性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]