Modeling BPEL and BPEL4People with a Timed Interruptable pi-Calculus

Author

Jin, Wei ; Wang, Hanpin ; Cao, Yongzhi ; Wang, Zizhen ; Ban, Xiaojuan

Author_Institution

Sch. of Electron. Eng. & Comput. Sci., Peking Univ., Beijing, China

fYear

2010

fDate

19-23 July 2010

Firstpage

487

Lastpage

492

Abstract

Business Processing Execution Language (BPEL) and BPEL for People (BPEL4People) are two web services orchestration languages for composing web services. To describe formally their semantics, we introduce the π_it-calculus, a new variant of the π-calculus, in this paper. The good feature of the π_it-calculus is that its execution can be interrupted and can handle timing events as well. We provide both syntax and semantics of the π_it -calculus and define a strong bisimulation relation that specifies when two processes can be considered as the same. With the new calculus, we then model the activities of BPEL and BPEL4People, and give their precise semantics. Our formal framework may facilitate the reliability and consistency analysis in a BPEL or BPEL4People design process.

Keywords

Web services; business data processing; pi calculus; specification languages; BPEL modelling; BPEL4People; Web services orchestration language; business processing execution language; timed interruptable π-calculus; Calculus; Context; Humans; Semantics; Syntactics; Timing; Web services; BPEL; BPELPeople; interruptable; pi-calculus; timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference (COMPSAC), 2010 IEEE 34th Annual

Conference_Location

Seoul

ISSN

0730-3157

Print_ISBN

978-1-4244-7512-4

Electronic_ISBN

0730-3157

Type

conf

DOI

10.1109/COMPSAC.2010.75

Filename

5676299