Title :
A Model Checking Tool Embedded into Services Composition Environment
Author :
Gao, Chunming ; Liu, Rongsheng ; Song, Yan ; Chen, Huowang
Author_Institution :
Coll. of Math. & Comput. Sci., Hunan Normal Univ., Changsha
Abstract :
This paper proposes a tool for formal verification of Web services composition based on an extended pi-calculus with type system and the conversion between BPEL and pi-calculus. This tool integrates three kinds of formal verification techniques, including open bisimulation, properties checking based on modal mu-calculus and the compatibility checking of composite Web services based on pi-calculus. With the combination checking techniques, the properties that service composition orchestration holds at abstract control flow level are checked, which achieve more completely validity checking about the orchestration. To check automatically, the automatic conversion between BPEL4WS and pi-calculus is introduced to this tool, and also the error slice for the orchestration are automatically marked. Further more, a novel method for discovering and matching web services is proposed, which is under the guidance of checking Web services compatibility
Keywords :
Web services; formal verification; page description languages; pi calculus; program testing; BPEL4WS; Web service composition; abstract control flow level; compatibility checking; extended pi-calculus; formal verification; modal mu-calculus; model checking tool; open bisimulation; properties checking; service composition environment; Assembly; Automatic control; Computer science; Concrete; Educational institutions; Formal verification; Mathematical model; Mathematics; Partial response channels; Web services; Pi-calculus type system web services Composition verification tool compatibility;
Conference_Titel :
Grid and Cooperative Computing, 2006. GCC 2006. Fifth International Conference
Conference_Location :
Hunan
Print_ISBN :
0-7695-2694-2
DOI :
10.1109/GCC.2006.11
