| ¡¡ | Chinese Journal of Computers Full Text |
| Title | Scenario-Based Analysis and Verification for Web Services Message Flows |
| Authors | YANG Lu LIU Xi WANG Lin-Zhang CHEN Xin LI Xuan-Dong |
| Address | (State Key Laboratory of Novel Software Technology, Nanjing University, Nanjing 210093) (Department of Computer Science and Technology, Nanjing University, Nanjing 210093) |
| Year | 2009 |
| Issue | No.9(1759¡ª1772) |
| Abstract & Background | Abstract 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 simplification 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 consistency 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. Keywords Web services; scenario-based specification; message interaction consistency checking |