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

摘要：

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

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

所属期刊栏目：33

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金;国家自然科学基金

在线出版日期：2022-08-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共15页

页码：2782-2796