面向基于场景规约的Web服务消息流分析与验证

Scenario-Based Analysis and Verification for Web Services Message Flows

采用UML顺序图构成基于场景的规约、WS-BPEL作为Web服务的描述语言,提出了一种面向基于场景规约对Web服务消息流进行分析与验证的方法:首先,对WS-BPEL消息流进行分析并将其自动抽象为基于Petri网的模型;同时,为了缩小状态空间、提高验证效率,在不影响消息交互顺序的前提下,对WS-BPEL源码和基于Petri网的模型分别进行化简,即面向基于场景规约将与验证无关的活动和元素删除;最后,通过遍历基于Petri网的模型以验证WS-BPEL消息流与基于场景的规约之间的一致性(消息交互顺序的存在/强制一致性).文中通过一个贯穿整个分析与验证过程的实例加以说明.该方法已经实现成为一个原型工具.

This paper purposes a scenario-based analysis and verification approach for the Web Services message flow, in which UML Sequence Diagrams are used to specify scenario-based specifications and WS-BPEL is used to describe Web Services designs. Firstly the authors analyze a WS-BPEL specification and automatically extract its message flow model expressed by a Petri net. At the same time, according to a given scenario-based specification the authors do the simpli- fication for both the WS-BPEL source code and the Petri net model to reduce the state space for efficient verification, i.e. removing the activities and process elements which are not concerned with the verification against the scenario-based specification. Finally, the authors verify the con- sistency between the WS-BPEL message flow and the scenario-based specification （existential/ mandatory consistency of message sequence） by traversing the Petri net model. A case study is given throughout the analysis and verification process to illustrate the approach. And a prototype tool is implemented to support this approach.