¡¡Chinese Journal of Computers   Full Text
  TitleDescribing and Verifying Web Service Using Pi-Calculus
  AuthorsLIAO Jun TAN Hao LIU Jin-De
  Address£¨College of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu 610054£©
  Year2005
  IssueNo.4(635¡ª643)
  Abstract &
  Background 		Using formal method is an effective methodology for modeling and verifying software system. Describing and verifying Web services by formal method is an important research. Guaranteeing the validity of Web services composition is necessary for enhancing the value of services. Pi-calculus is a kind of mobile process algebra which can be used to model concurrent and dynamic systems. Web services and their composition are described and modeled based on Pi-calculus in this paper. Some difference among the Pi-calculus and other formal methods is discussed. Rules about applying Pi-calculus to Web services are explained and the method of working out agents and channels is proposed. Relationship between Pi-calculus and Web services protocol stack is illustrated too. Finally, a demo is constructed and the validity of composition model is verified. Compared to process algebra method based on CCS, the Pi-Calculus can be used for describing and reasoning dynamic system and appropriate for modeling Web services composition.

keywords Pi-calculus£» process algebra£» Web service£» service composition£» formal service