Describing and Verifying Web Service Using Pi-Calculus
Describing and Verifying Web Service Using Pi-Calculus
复制标题
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Liao Jun
中科院分区：
文献类型：
--
作者：
Liao Jun
形式化方法是对软件系统进行建模和验证的有效方法。用形式化方法描述和验证Web服务是一个重要的研究课题。保证Web服务组合的有效性是提高服务价值的必要条件。Pi演算是一种移动的进程代数，可用于对并发和动态系统进行建模。基于Pi演算对Web服务及其组合进行了描述和建模。讨论了Pi演算与其它形式化方法的区别。阐述了Pi演算在Web服务中的应用规则，提出了确定代理和通道的方法。同时还说明了Pi演算与Web服务协议栈的关系。最后，通过一个实例验证了组合模型的有效性.与基于CCS的进程代数方法相比，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.