Paper Info
Title
Model Checking WS-BPEL with Universal Modal Sequence Diagrams
Abstract
Analyzing the composite service by manual is rather difficult and time-consuming. In the paper, we propose an approach to automatically verify the correctness of composite services by model checking based on a novel property specification universal Modal Sequence Diagrams(uMSDs). Because uMSDs can find a well-balance between simplicity of use and expressive power, the temporal properties of the composite service can be specified by uMSDs in an easy and intuitive way. Based on the formal syntax and semantics of uMSDs, a novel model checking approach is proposed to verify whether the model of WS-BPEL specification satisfies the properties represented by uMSDs. Finally, a series of experiments show the approach can effectively detect the logical errors in an On-the-Job Assistant case study.
Year
DOI
Venue
2011
10.1109/ICIS.2011.58
ACIS-ICIS
Keywords
Field
DocType
composite service,model checking ws-bpel,formal syntax,ws-bpel specification,model checking,logical error,novel model checking approach,temporal property,novel property specification,expressive power,universal modal sequence diagrams,on-the-job assistant case study,automata,semantics,unified modeling language,business
Sequence diagram,Programming language,Model checking,Unified Modeling Language,Computer science,Correctness,Automaton,Theoretical computer science,Business Process Execution Language,Formal grammar,Modal
Conference
Citations 
PageRank 
References 
0
0.34
9
Authors
4
Name
Order
Citations
PageRank
Wenrui Li1588.98
Zhongxue Yang2122.37
Pengcheng Zhang315310.70
Wang Zhijian410627.49