论文部分内容阅读
目的 为了保证使用商业过程执行语言（BPEL）描述的Web服务组合的正确性。方法用着色Petri网（CP-nets）对BPEL流程进行建模、分析以及验证。结果定义了一套从BPEL到CP-nets的映射规则，该规则可以将BPEL流程转换成CP-nets，通过着色Petri网工具-CPNtools对该CP-nets进行自动分析以及验证，从而验证该BPEL流程的安全性、活性等性质。结论利用CP-nets这种形式化工具可以有效地发现BPEL流程中存在的设计错误。