基于Pi-演算的服务组合正确性验证

Verifying the Accuracy of Web Services Using Pi-calculus

对于Web服务及其组合而言,保证其正确性并实现增值服务是十分必要的。Pi-演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模。通过建立一个实际的模型,用Pi-演算对Web服务及其组合进行建模,并利用形式化工具对建立的组合模型是否正确以及是否满足需求进行了验证。

Guaranteeing the accuracy of Web services and their composition is necessary to achieve value-added services. Pi-calculus is a kind of mobile process algebra which can be used to model the concurrent and dynamic changes system. A demo is constructed in this paper; the Web services and their composition are modeled based on Pi-calculus; the validity of composition model and whether it meets the need are verified using formal tools.