PiFF: A formal framework for dynamic service composition

Author

Tan Hao ; Liu Jin-De ; Liao Jim

Author_Institution

Univ. of Electron. Sci. & Technol. of China, Chengdu

fYear

2007

fDate

11-13 July 2007

Firstpage

515

Lastpage

520

Abstract

Service choreography and orchestration are two views of the service compositions. In order to select and compose services correctly, some formal methods and tools are used to model and verify those compositions. Pi calculus is a major theory of process algebra that can be used as the formal basis of service composition. According to analysis result of WS CDL and WS BPEL, PiFF - a formal verification framework based on pi calculus is proposed which can be used to check and validate service composition both from global and local point of views. PiFF constitutes of three parts: mapping, methods and tools. This framework can promise consistency between WS CDL and WS BPEL and guarantee developing of dynamic service composition correctly by concept of weak bisimulation.

Keywords

Web services; formal verification; pi calculus; PiFF; WS BPEL; WS CDL; dynamic service composition; formal methods; formal verification; pi calculus; process algebra; service choreography; service orchestration; Calculus; Computational modeling; Switches; Transforms;

fLanguage

English

Publisher

ieee

Conference_Titel

Communications, Circuits and Systems, 2007. ICCCAS 2007. International Conference on

Conference_Location

Kokura

Print_ISBN

978-1-4244-1473-4

Type

conf

DOI

10.1109/ICCCAS.2007.6251628

Filename

6251628