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

来源：软件学报杂志2022年第8期北京时间：

作者：赵樱，谭锦豪，李国强

单位：赵樱，上海交通大学 软件学院, 上海 20024011,谭锦豪，上海交通大学 软件学院, 上海 20024002,李国强，上海交通大学 软件学院, 上海 20024003

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

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

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