论文部分内容阅读
采用UML顺序图构成基于场景的规约、WS—BPEL作为Web服务的描述语言，提出了一种面向基于场景规约对Web服务消息流进行分析与验证的方法：首先，对WS—BPEL消息流进行分析并将其自动抽象为基于Petri网的模型；同时，为了缩小状态空间、提高验证效率，在不影响消息交互顺序的前提下，对WS—BPEL源码和基于Petri网的模型分别进行化简，即面向基于场景规约将与验证无关的活动和元素删除；最后，通过遍历基于Petri网的模型以验证WS-BPEL消息流与基于场景的规约之间的一致性（消息交互顺序的存在／强制一