Research on Formal Modeling and Verification of BPEL-based Web Service Composition

Author

Zhao, Huiqun ; Wang, Wenwen ; Sun, Jing ; Wei, Ying

Author_Institution

Dept. of Comput. Sci., North China Univ. of Technol., Beijing, China

fYear

2012

fDate

May 30 2012-June 1 2012

Firstpage

631

Lastpage

636

Abstract

With the development of Web Service composition, more and more diversified and complex business demands are satisfied. But the logical validity cannot be guaranteed. After a short view of recent research efforts of formal modeling and verification about Web Service, this paper proposes a new formal model for WS-BPEL described Web Service composition. The specification language of the model is LOTOS. Model checking is adopted to ensure the validity of this model. Finally, an example is presented to illustrate the practicality of the model.

Keywords

Web services; business data processing; formal verification; specification languages; BPEL-based Web service composition; LOTOS; WS-BPEL; business process execution language; complex business demands; formal modeling; formal verification; logical validity; model checking; model specification language; model validity; Algebra; Automata; Business; Calculus; Protocols; Safety; Web services; BPEL; LOTOS; Web Service; formal description model; model checking;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer and Information Science (ICIS), 2012 IEEE/ACIS 11th International Conference on

Conference_Location

Shanghai

Print_ISBN

978-1-4673-1536-4

Type

conf

DOI

10.1109/ICIS.2012.92

Filename

6211163