论文部分内容阅读
Web服务是一种新型的分布式的计算模型，可以在多种异构平台的基础上构建一个通用的、无关平台的、无关语言的技术层，使得不同平台之上的应用更为方便地进行连接和集成，具有更好的开放性，是建立可互操作的分布式应用程序新的平台。 随着Web服务技术的快速发展和应用，单一的Web服务由于功能有限，所以往往采用Web服务组合的方法来生成功能复杂且满足应用需求的Web服务。然而在研究Web服务组合的过程中，如何使用进程代数来形式化的对Web服务组合进行描述并且验证Web服务组合的正确性是一个关键性问题，因为流程的正确性问题必须在它正式实施前得到形式上的建模与验证。 本文分析了Web服务组合验证的必要性，比较了Web服务组合的验证方法，并采用Pi-演算对Web服务及其组合进行形式化的建模和描述。在简单介绍了Web服务及Web服务组合相关的理论和技术之后，深入地研究了Pi-演算的语法定义和结构等价、行为等价理论，给出了Web服务协议栈和Pi-演算的对应关系，提出了基于Pi-演算的服务组合验证方法。 最后利用Pi-演算的方法对电子购物系统的服务及其组合进行了形式化的建模和描述，通过一款针对Pi-演算开发的自动验证工具MWB对Web服务组合模型的正确性进行了验证。