Automated Analysis and Implementation of Composed Grid Services

Citation

Tan KLL & Turner KJ (2007) Automated Analysis and Implementation of Composed Grid Services. In: Dranidis D & Sakellariou I (eds.) SEEFM07: Proceedings of the 3rd South-East European Workshop on Formal Methods. SEEFM07 - 3rd South-East European Workshop on Formal Methods, Thessaloniki, Greece, 30.11.2007-01.12.2007. Thessaloniki: South-East European Research Centre, pp. 51-64. http://www.seefm.info/workshops.html

Abstract
Service composition allows web services to be combined into new ones. Web service composition is increasingly common in mission-critical applications. It has therefore become important to verify the correctness of web service composition using formal methods. The composition of grid services is a similar but new goal. We have previously developed an abstract graphical notation called CRESS for describing composite grid services. We have demonstrated that it is feasible to automatically generate service implementations as well as formal specifications from CRESS descriptions. The automated service implementations use orchestration code in BPEL, along with the service interfaces and data types in WSDL and XSD respectively for all services. CRESS-generated BPEL implementations currently do not useWSRF features such as implicit endpoint references for WS-Resources and interfacing to standard WSRF port types. CRESS-generated formal models use the standardised process algebra LOTOS. Service behaviour is modelled by processes, while service data types are modelled as abstract data types. Simulation and validation of the generated LOTOS specifications can be performed. In this paper, we illustrate how CRESS can be further extended to improve its generation of service compositions, specifically for WSRF services implemented using Globus Toolkit 4. We also show how to facilitate use of the generated LOTOS specifications with the CADP toolbox.