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

Polyadic Pi-Calculus Based Description and Verification for Web Service

验证问题是Web服务发展中亟待解决的关键问题之一,类型系统的加入以及Web服务动态的体系结构给问题的解决增添了很多难度.针对上述问题,在多元Pi-演算的基础上给出Web服务的描述模型和子类型关系定义,并对Web服务的相容性进行细化,给出Web服务可替换性定义;基于这些模型和定义,给出Web服务构造时类型正确性的判定规则和运行时可替换性的判定方法;最后用1个例子说明上述规则和方法的可行性.结果表明上述模型、定义和方法为解决动态的、类型化的Web服务验证问题提供了理论依据和基础.

Verification is one of the important issues to be addressed in the development of Web services, and type system and the dynamic architecture of Web services, add a lot more difficulty to it. This paper gives the description model of Web services and the subtype relationship defined on the basis of polyadic Pi-calculus, and defines replace-ability to refine the concept of compatibility. Based on the above models and definitions, this paper addresses the rules to determining type correctness at construction time of Web services and the method of determining replace-ability at run time. Finally, an example illustrates the feasibility of the above-mentioned rules and methods. All of the definitions and methods established in this paper provide a theoretical basis and foundation for solving dynamic and typed Web service verification.