Enhanced Version of the CRESS Tool for Analyzing Composed Grid Services

Organisation:	University of Stirling (UNITED KINGDOM)
Functionality:	Analysis of composed grid services.
Tools used:	CADP (Construction and Analysis of Distributed Processes) GT4 ActiveBPEL TOPO/LOLA
Period:	2007-2012
Description:	Grid computing enables interoperability between disparately owned and heterogeneous resources in a standardised manner. The SOA (Service-Oriented Architecture) nature of grid services encourages the creation of new and composite services by combining existing services into new ones. This activity, known as orchestration, requires complex behaviour involving interactions between two or more grid services. Although there is much interest in the practical realisation of grid service orchestration, the rigorous analysis of such complex and usually critical behaviour using, e.g., formal methods, has not received much attention. This work attempts to bridge the model-implementation gap to allow both for automated formal analysis as well as implementation of grid and Web services. Occupational information is used by social scientists to perform various kinds of analyses and surveys. Aggregate occupational datasets, which contain summary data for occupational position, are often linked by social scientists to microsocial survey datasets. Occupational information has to be translated (often by applying several translation steps) into the classifications required by the analysis process. Hence there exist many translation procedures for dealing with various formats. Despite having occupational data and mapping resources, social scientists rarely achieve effective resource sharing due to a lack of a standardised framework for resource discovery, dissemination and data formats. The GEODE (Grid-Enabled Occupational Data Environment) project aims at using grid computing to vitalise occupational matching procedures and make them discoverable and accessible in a uniform manner. CRESS (Communication Representation Employing Systematic Specifications) is a domain-independent graphical notation that was developed for describing services. CRESS supports the specification of Web and grid service composition. It takes an abstract approach in which a high-level CRESS service description is used to automatically generate a formal specification as well as an actual implementation. The implementations of composite grid services, service interfaces, and data types are generated in BPEL, WSDL, and XSD, respectively. The formalisation of a composite grid service in LOTOS is completely automated: service behaviour is represented by interacting LOTOS processes and data types are represented as LOTOS abstract data types. CRESS is designed as an extensible framework where support for new domains and target languages can be added like plug-ins. The LOTOS specifications generated automatically from CRESS grid service descriptions are preprocessed using TOPO/LOLA in order to expand parameterized data types. Then, CADP-specific annotations are added for bounding the domains of data types and obtain configurations with state spaces of reasonable size. The annotated LOTOS specifications are subsequently analyzed using CADP. The CAESAR and CAESAR.ADT compilers are used for generating the state spaces underlying the LOTOS specifications, and the EVALUATOR tool was used to check various properties, the whole process being automated using SVL scripts. Several properties are of interest for Web/grid services managing occupational data: absence of deadlock, presence of results or faults after requests, absence of successful results if the input contains wrong occupation values, presence of correct mapping of occupational values. EVALUATOR allowed to discover a violation of the fourth property, which was due to an erroneous mapping specification for a particular occupational value. Although this error might have been found using testing, this would have required an exhaustive set of tests that explored the entire state space.
Conclusions:	The techniques developed for verifying CRESS-generated descriptions have yielded favourable results. Coupled with automated annotation for CADP, formal verification of CRESS descriptions is now a practical task. Future work concerns the enhancement of CRESS to improve its support of orchestrated grid services and the further automation of the process of making a LOTOS specification ready for verification. As regards grid services, CRESS appears to be a useful approach for service orchestration and formal analysis.
Publications:	[Tan-Turner-07] Koon Leai Larry Tan and Kenneth J. Turner. "Automated Analysis and Implementation of Composed Grid Services". Proceedings of the 3rd South-East European Workshop on Formal Methods, pp. 51-64, November 2007. Full version available on-line from http://www.cs.stir.ac.uk/~kjt/research/pdf/comp-grid.pdf or from the CADP Web site in PDF or PostScript [Turner-Tan-09] Kenneth J. Turner and Koon Leai Larry Tan. "A Rigorous Methodology for Composing Services". Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2009, Lecture Notes in Computer Science vol. 5825, pages 165-180. Springer Verlag, November 2009. Available on-line from http://www.cs.stir.ac.uk/~kjt/research/pdf/form-comp.pdf or from the CADP Web site in PDF or PostScript [Tan-09-a] Koon Leai Larry Tan. "An Integrated Methodology for Creating Composed Web/Grid Service". Thesis, December 2009. Available on line from http://hdl.handle.net/1893/2515 or from the CADP Web site in PDF or PostScript [Turner-Tan-12] Kenneth J. Turner and Koon Leai Larry Tan. "Rigorous Development of Composite Grid Services". Network and Computer Applications, 35(4):1304-1316, February 2012. Available on line from http://www.cs.stir.ac.uk/~kjt/research/pdf/rig-dev.pdf or from the CADP Web site in PDF or PostScript
Contact:	Kenneth J. Turner Computing Science and Mathematics University of Stirling Stirling FK9 4LA Scotland Tel: +44 1786 467 423 Fax: +44 1786 464 551 Email: kjt@cs.stir.ac.uk
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page