Pi-calulus Based Formal Description Model For Web Services

Web service composition allows developers to compose numerousservices to solve complex problem based on service-oriented distributedcomputing. Most Web services are developed independently and runningon heterogeneous platforms, in order to achieve the combination ofservices between them, service composition description method andverification(testing) method are need to compatible with heterogeneous.This paper summarizes the results of previous study, establish the formaldescription model PiFM4WS of Web services based on Pi-calculus. TheWeb service and the main acts of Web service composition are describedin the model mentioned above, and a unified description method isproposed for dynamic Web service composition architecture. Differentperspectives based Web service composition description specificationsare mapped to PiFM4WS main acts, and the equivalence betweendifferent descriptions after mapping is proofed. The PiFM4WS model hastype system to refine Web services compatibility, and support the conceptof replaceability and verification methods. The PiFM4WS model is usedto describe the service network, and provide theoretical basis of the Webservice automation composition. The main research results obtained areas follows:(1) Establish formal description model PiFM4WS of Web services. ThePiFM4WS syntax structure definition provides description of external andinternal behavior of Web services. The PiFM4WS isomorphic rules andoperational semantics provide the interactions behaviors occur throughWeb service combination.(2) Provides mapping rules for the description of main behavioral of twodifferent perspectives: The description methods of PiFM4WS areprovided for the concepts and acts of BPEL4WS specification andWS-CDL specification. The equivalence of different specifications isproofed from the perspective of syntax and operational semantics. Thedynamic architecture description method provided in PiFM4WS, can notbe achieved in other existing models.(3) Provides Web services composition validation based on typed model PiFM4WS. The type system is added to PiFM4WS, and base on it,replaceability definition is proposed according to the relationship betweensubtypes and refines Web service compatibility. Replaceabilityverification method under the dynamic architecture of Web services isproposed according to the channel classification of process-related andcombining Pi-calculus substitution algorithm.(4) Formal description of the service network provides a theoretical basisof automatic Web service composition. The communication channelstructure between abstract services and concrete services is abstracted anddescribed, which establish theoretical foundation of the formaldescription of service relationship.In summary, this paper presents the formal description model PiFM4WS,the typed PiFM4WS and formal description of service network provide aunified formal description and verification framework, and providetheoretical basis for Web services automatic composition.