基于Pi-演算的Web服务组合的描述和验证  

Describing and Verifying Web Service Using Pi-Calculus

作　　者：廖军[1] 谭浩[1] 刘锦德[1] 

机构地区：[1]电子科技大学计算机科学与工程学院,成都610054

出　　处：《计算机学报》2005年第4期635-643,共9页Chinese Journal of Computers

基　　金："十五"国防预研项目基金(41315010103)资助.

摘　　要：形式化方法对于建模和验证软件系统是一种有效的方法,所以对 Web服务的形式化描述和验证是一个重要的研究方向.对于Web服务及其组合来说,保证其组合正确性以实现其服务增值是十分必要的.Pi 演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模.该文基于 Pi 演算对 Web服务及其组合进行形式化描述和建模.文中说明了Pi 演算与以前形式化方法的不同之处,分析了Pi 演算应用于Web服务组合需要解决的问题.讨论了Pi 演算与Web服务协议栈的对应关系,说明了利用Pi 演算建立 Web服务组合模型的规则,指出了如何寻找代理和通道.最后建立了一个实际的模型,并利用形式化工具对建立的组合模型是否正确以及是否满足需求进行了验证.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.

关 键 词：PI-演算 进程代数 WEB服务 服务组合 服务形式化 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]