PVS based Petri Nets Verification and Its Application in Workflow
The major problem in verifying petri nets is the state explosion. In this paper we showed that the theorem prover PVS can be used to verify Petri Nets. In PVS, Petri net is viewed as a state machine, properties are expressed with invariants. Verification is accomplished by induction proof which makes us avoid the state explosion. Soundness is a very important property in workflow. We further showed that the soundness can also be verified by induction on the transition which makes possible to verify large workflow process.
PVS Petri net workflow soundness
Yuzhong Wang Conghua Zhou
School of An Jiangsu University Zhenjiang 212013,China School of Computer Scienceg Jiangsu University Zhenjiang 212013,China
国际会议
成都
英文
1451-1455
2010-12-17（万方平台首次上网日期，不代表论文的发表时间）