| 基于通信Petri网的异步通信程序验证模型 |
| |
| 引用本文： | 杨启哲,李国强.基于通信Petri网的异步通信程序验证模型[J].软件学报,2017,28(4):804-818. |
| |
| 作者姓名： | 杨启哲 李国强 |
| |
| 作者单位： | 上海交通大学软件学院, 上海 200240,上海交通大学软件学院, 上海 200240 |
| |
| 基金项目： | 国家自然科学基金（61672340，61472238，91318301） |
| |
| 摘 要： | 由于多栈的模型图灵等价，因此通用的异步通讯程序模型的验证问题不可判定.为此，基于Petri网，提出了一个新的模型通讯——通讯Petri网对异步通讯程序进行刻画，通过对输入通讯进行k-型限制，以及对每个栈进行基于正则语言泵引理的抽象，通过将这样限制下的模型编码到数据Petri网，证明了限制下的新模型可覆盖性可判定.
|
| 关 键 词： | 异步通讯程序 通讯Petri网 可覆盖性 程序验证 k-型 |
| 收稿时间： | 2016/5/27 0:00:00 |
| 修稿时间： | 2016/11/26 0:00:00 |
Model on Asynchronous Communication Program Verification Based on Communicating Petri Nets |
| |
| YANG Qi-Zhe and LI Guo-Qiang.Model on Asynchronous Communication Program Verification Based on Communicating Petri Nets[J].Journal of Software,2017,28(4):804-818. |
| |
| Authors: | YANG Qi-Zhe and LI Guo-Qiang |
| |
| Affiliation: | School of Software, Shanghai JiaoTong University, Shanghai 200240, China and School of Software, Shanghai JiaoTong University, Shanghai 200240, China |
| |
| Abstract: | Since multi-stack models are generally Turing-complete, verification problems on general models for asynchronously communicating programsare undecidable. This paper proposes a new model based Petri net, named communication Petri nets (C-Petri nets) to model asynchronously communicating programs. Applying the k-shaped restriction on the input communications and the abstraction on each stack based on popping lemma of regular languanges, the coverability problem of the restricted C-Petri net is decidable, by encoding the model to data Petri nets. |
| |
| Keywords: | asynchronously communicating program communication Petri nets coverability program vertification k-shaped |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
