论文部分内容阅读
目前，业务流程执行语言BPEL作为描述web服务组装的语言已经被广泛接受。但是由于BPEL是用XML表示，自然语言描述其语义，缺乏形式化，很容易在设计中引入不易发觉的错误。对于企业来说，很多BPEL涉及数额庞大的交易，任何设计错误都可能带来巨大损失，事后的修复在时间上和成本上都可能付出巨大的代价。因此有必要在部署流程之前，对流程的正确性进行建模和分析。
本文使用一种具有强大描述能力的高级Petri网--Cnet来建模BPEL的控制流。本文的建模范围涵盖BPEL控制流的所有元素，不但包括了基本和结构化活动，而且建模了作用域以及相关的错误、补偿、事件和终止处理。本文还刻画了BPEL中的死路删除，特别是作用域的正常行为和错误处理的死路删除。在从BPEL到Cnet的转换中，本文为每个元素的映射提供了统一的接口，这样对于任意给定的BPEL流程，可以先把各组成部分按照本文的Cnet模型转换，再通过统一的接口进行组装。最后本文提出了正确的BPEL流程应该具有的两个性质--畅通性和无冗余性，并给出了利用可达图来验证这些性质的方法。