| Model Checking Workflow Net Based on Petri Net |
| |
| 引用本文： | ZHOU Conghua CHEN Zhenyu. Model Checking Workflow Net Based on Petri Net[J]. 武汉大学学报:自然科学英文版, 2006, 11(5): 1297-1301. DOI: 10.1007/BF02829255 |
| |
| 作者姓名： | ZHOU Conghua CHEN Zhenyu |
| |
| 作者单位： | [1]School of Computer Science and TelecommunicationEngineering, Jiangsu University, Zhenjiang 212013, Jiangsu,China [2]School of Computer Science and Engineering,Southeast University, Nanjing 210096, Jiangsu, China |
| |
| 摘 要： | The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic ＊ （CTL ＊ ） can be used to character the relaxed soundness of the workflow.
|
| 关 键 词： | 工作流 模型校验 CTL 皮特里网 |
| 文章编号： | 1007-1202（2006）05-1297-05 |
| 收稿时间： | 2006-03-25 |
Model checking workflow net based on Petri net |
| |
| Zhou Conghua,Chen Zhenyu. Model checking workflow net based on Petri net[J]. Wuhan University Journal of Natural Sciences, 2006, 11(5): 1297-1301. DOI: 10.1007/BF02829255 |
| |
| Authors: | Zhou Conghua Chen Zhenyu |
| |
| Affiliation: | (1) School of Computer Science and Telecommunication Engineering, Jiangsu University, 212013 Zhenjiang, Jiangsu, China;(2) School of Computer Science and Engineering, Southeast University, 210096 Nanjing, Jiangsu, China |
| |
| Abstract: | The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic (CTL) allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic* (CTL*) can be used to character the relaxed soundness of the workflow. |
| |
| Keywords: | model checking computation tree logic * (CTL * ) Petri nets workflow |
| 本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录！ |
