文档介绍：南京邮电大学
硕士学位论文
基于Pi-演算的Web服务组合的描述和验证
姓名:常斌
申请学位级别:硕士
专业:计算机应用技术
指导教师:杨庚
2011-03
南京邮电大学硕士研究生学位论文` 摘要
摘要
在研究 Web 服务组合中存在着一个重要问题是怎么样使用进程代数形式化的描述
Web服务组合并且证明 Web服务组合的正确性。用 Pi-演算建模 Web服务组合的模型可以
用来检查、验证 Web服务组合以保证服务组合的正确性。因为 Web服务组合关联到很多
的 Web服务通信协作,这一特征让 Web服务组合的验证工作更加艰难。同时 Web服务语
言是一种基于业务流程的服务组合方法(BPEL4WS),建模理论基础比较薄弱,组合正确
性的保证较弱。所以流程的无死锁性、正确性等问题,在它正式被实施前必须得到形式上
的建模与检验。
对于建模和验证软件系统来说,形式化方法是一种有效的方法,所以对 Web服务组合
的形式化验证和描述是一个关键的研究领域。保证 Web服务组合的正确性以实现服务增值
对于 Web服务及其组合来说是非常重要的。本文通过 Pi-演算来形式化建模和描述 Web服
务及其组合。文中涉及了 Web服务协议栈与 Pi-演算的对应关系,同时通过使用 Pi-演算建
模 Web服务组合的规则,说明了怎么样发现通道和代理。文章最后建立了一个实际的模型,
并利用形式化工具对建立的组合模型是否正确以及是否满足需求进行了验证。同时运用了
Pi-演算互模拟理论对 Web服务组合的相容性、行为等价性进行了验证。
关键字:Pi-演算;Web服务组合;行为等价
I
南京邮电大学硕士研究生学位论文` Abstract
Abstract
One of an important question in web position researching area is how to
describe Web position formally and verify the correctness of Web service
composition. Using Pi-calculus model position can be used to check and verify
position in order to ensure the correctness of position. Because
position of Web services munication and collaboration of several Web
service, this feature makes the verification of position of Web service more difficult.
Besides, the Business Process Execution Language for Web services (BPEL4WS) as to be a
position method, which is based on business process, is weak in modeling, and the
assurance of the validity is also weak. So the validity of the process and the property of
non-deadlocks must be simulated and proved before being implemented formally.
Using formal method is an effective way for modeling and verifying software system.
Describing and verifying WebServices by formal method is an important research. Guaranteeing
the validity of Web services is very important for enhancing the value of services. Web services
and position are described and modeled based on Pi-calculus in this paper. Rules about
applying Pi-calculus to Web services are explained and the method of working ou