摘要
目的为了保证使用商业过程执行语言(BPEL)描述的Web服务组合的正确性。方法用着色Petri网(CP-nets)对BPEL流程进行建模、分析以及验证。结果定义了一套从BPEL到CP-nets的映射规则,该规则可以将BPEL流程转换成CP-nets,通过着色Petri网工具-CPN tools对该CP-nets进行自动分析以及验证,从而验证该BPEL流程的安全性、活性等性质。结论利用CP-nets这种形式化工具可以有效地发现BPEL流程中存在的设计错误。
Aim To ensure the correctness of Web service composition described by BPEL. Methods The Colored Petri nets （CP-nets） are employed to modeling, analysis and verifying BPEL processes. Results A given BPEL process can be transformed into CP-nets with a set of translation rules. By implementing CPN tools, the properties of the given BPEL processes, such as security and liveness, can be verified. Conclusion By utilizing CP- nets, the design flaws of BPEL processes can be found effectively.
出处
《西北大学学报（自然科学版）》
CAS
CSCD
北大核心
2007年第6期986-990,共5页
Journal of Northwest University（Natural Science Edition）
基金
国家自然科学基金资助项目(60373103)
高等学校博士学科点专项科研基金资助项目(20030701015)
