基于通信Petri网的异步通信程序验证模型
来源：软件学报杂志2017年第4期北京时间：
作者：杨启哲,李国强
单位：杨启哲，上海交通大学 软件学院, 上海 20024011,李国强，上海交通大学 软件学院, 上海 20024002
摘要：由于多栈的模型图灵等价，因此，通用的异步通信程序模型的验证问题不可判定.为此，基于Petri网，提出了一个新的模型通信——通信Petri网，对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象，通过将这样限制下的模型编码到数据Petri网，证明了限制下的新模型可覆盖性可判定.
关键词：异步通信程序;通信Petri网;可覆盖性;程序验证;k-型
基金资助：国家自然科学基金（61672340，61472238，91318301）
