典型文献
基于基本并行进程的异步通信程序的验证方法
文献摘要：
异步通信程序是进程间通过异步消息通信实现非阻塞并发的程序.当前异步通信程序的程序验证问题通常将其归约至向量加法系统及其扩展模型,因而复杂度很高,缺乏高效工具.基本并行进程作为向量加法系统的一个子类,其可达性的验证问题为NP完备.首先,改进了Osualdo等人提出的为异步通信程序建模的Actor通信系统,将其归约至基本并行进程.然后,实现了基本并行进程的模型检测工具RABLE,实验结果表明,验证方法在异步通信程序的一系列程序验证问题上具有比已有工具更高效的结果.
文献关键词：
异步通信程序;基本并行进程;Actor通信系统;模型检测;可达性
中图分类号：
作者姓名：
赵樱;谭锦豪;李国强
作者机构：
上海交通大学 软件学院, 上海 200240
文献出处：
引用格式：
[1]赵樱;谭锦豪;李国强-.基于基本并行进程的异步通信程序的验证方法)[J].软件学报,2022(08):2782-2796
A类：
基本并行进程,异步通信程序,Osualdo,RABLE
B类：
验证方法,通信实现,程序验证,归约,加法,法系,扩展模型,而复,子类,可达性,NP,Actor,通信系统,模型检测,检测工具
AB值：
0.158252
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
