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

摘要

在研究Web 服务组合中存在着一个重要问题是怎么样使用进程代数形式化的描述Web 服务组合并且证明Web 服务组合的正确性。用Pi-演算建模Web 服务组合的模型可以用来检查、验证Web 服务组合以保证服务组合的正确性。因为Web 服务组合关联到很多的Web 服务通信协作，这一特征让Web 服务组合的验证工作更加艰难。同时Web 服务语言是一种基于业务流程的服务组合方法（BPEL4WS），建模理论基础比较薄弱，组合正确性的保证较弱。所以流程的无死锁性、正确性等问题，在它正式被实施前必须得到形式上的建模与检验。
　　 对于建模和验证软件系统来说，形式化方法是一种有效的方法，所以对Web 服务组合的形式化验证和描述是一个关键的研究领域。保证Web 服务组合的正确性以实现服务增值对于Web 服务及其组合来说是非常重要的。本文通过Pi-演算来形式化建模和描述Web 服务及其组合。文中涉及了Web 服务协议栈与Pi-演算的对应关系，同时通过使用Pi-演算建模Web 服务组合的规则，说明了怎么样发现通道和代理。文章最后建立了一个实际的模型，并利用形式化工具对建立的组合模型是否正确以及是否满足需求进行了验证。同时运用了Pi-演算互模拟理论对Web 服务组合的相容性、行为等价性进行了验证。

目录

文摘

英文文摘

声明

第一章引言

第二章Web 服务及其组合

第三章Pi-演算概述

第四章Web 服务组合的Pi-演算建模

第五章Web 服务组合的建模验证

第六章结语

致谢

参考文献

攻读硕士期间参加的项目

作者在研究生期间发表的论文