Modeling BPEL and BPEL4People with a Timed Interruptable π-Calculus
Meixia Zhu · Beijing Daxue Xuebao. Zirankexueban · 2012
To describe formal semantics of business processing execution language(BPEL) and BPEL for people(BPEL4People),the authors introduce the πit-calculus,a new variant of the π-calculus.The execution of πit-calculus can be interrupted and can handle timing events as well.Both syntax and semantics of the πit-calculus are provided.A strong bisimulation relation that specifies when two processes can be considered as the same is also given.The activities of BPEL and BPEL4People are modeled by the new calculus.The formal framework may facilitate the reliability and consistency analysis in BPEL or BPEL4People design process.