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

被引：101

作者：

廖军

谭浩

刘锦德

机构：

[1] 电子科技大学计算机科学与工程学院

来源：

计算机学报 | 2005年 / 04期

关键词：

Pi-演算; 进程代数; Web服务; 服务组合; 服务形式化;

D O I：

暂无

中图分类号：

TP393.09 [];

学科分类号：

080402 ;

摘要：

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

引用

页码：635 / 643

页数：9