支持Web服务组合与验证的形式化模型

Formal model supporting Web service composition and verification

针对Web服务的组合与验证问题,在范畴理论描述框架的基础上,引入进程代数描述服务组件的外部行为,为Web服务系统的架构描述建立了一种形式化的语义模型。Web服务作为范畴理论中的对象节点,服务间的交互和组合关系作为态射,从而以范畴图表的形式来描述服务网络。在形式化定义服务接口、Web服务、服务组合等概念的基础上,进一步分析讨论了服务组合和交互过程中的语义特性,给出了Web服务可替代性和服务请求可满足性的形式化定义。实例研究表明,该框架增强了Web服务架构的语义描述能力。

To solve the problems of Web service composition and verification, a formal model was proposed based on the framework of category theory. Process Algebra was introduced into the framework to describe the external behavior of service component, establishing a formal semantic model for the architecture of Web service system. The service network was described with category diagrams, in which Web services were used as categorical objects, and the interactive and composition relationships between services were used as morphisms. On the basis of the formal definitions of service interface, Web service and service composition, a further analysis and discussion about the semantics of service composition and interaction was undertaken. The concepts on Web service substitutability and service request satisfiability were formally defined. The application research shows that the proposed framework enhances semantic description capabilities of Web service architecture.