Automated Formal Analysis of CRESS Web and Grid Services

Organisation:	University of Stirling (UNITED KINGDOM)
Method:	CRESS LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Web Services.
Period:	2009
Size:	n/a
Description:	Web and grid services are distributed applications based on a loose coupling of functionality and interoperability in heterogeneous environments, typically using standards such as SOAP (Simple Object Access Protocol) and WSDL (Web Services Description Language). Web and grid services are widely used in businesses and research, where they are often mission-critical. Services can be combined to create new services; this is known as service composition. Formal methods are increasingly necessary as the complexity of services and their compositions grows, to validate system specifications and detect errors prior to implementation, minimising the potential cost. 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, by generating an annotated LOTOS specification that can be validated using CADP. Two cases studies, a web service and a grid service, using CRESS and its associated tools are presented. The web service example consists of three composite business services: CarMen is a car purchase broker, dealing with ordering a car. It is composed of the DoubleQuote service for supplying cars, which uses the BigDeal and WheelerDealer services, both of which provide quotation, ordering, and cancellation services, and the LoanStar financing services, which uses the FirstRate service for evaluating, accepting, or rejecting load requests and setting the interest rate, and the RiskTaker service for loan risk assessment. The grid service example deals with the occupational research sub-discipline of social science, specifically looking at analysis of occupational data. The Allocator service is a typical social science workflow preparing data for analysis by mapping the data according to a classification scheme. The Allocator is composed of two services, Factory, which allocates resources containing occupational scheme information, and Mapper, which performs the actual mapping of occupations using the allocated resources. The basic methodology for both case studies is essentially the same. Each service is specified in a CRESS diagram, from which the formal specification is automatically generated. The service specifications are validated using MUSTARD scenarios, validating first the component services and then their composition. The annotated specification is then verified using the CADP tools, the whole process being automated using SVL scripts.
Conclusions:	These case studies demonstrate successful use of the methodology for applying formal methods to web and grid services. The tools used are presented in http://cadp.inria.fr/software/07-h-cress.html
Publications:	[Tan-09-b] Koon Leai Larry Tan. "Case Studies Using CRESS to Develop Web and Grid Services". Technical Report CSM-183, University of Stirling, December 2009. Available on-line at: http://www.cs.stir.ac.uk/~kjt/techreps/pdf/TR183.pdf or from the CADP Web site in PDF or PostScript
Contact:	Prof. Kenneth J. Turner Department of Computing Science and Mathematics University of Stirling Stirling FK9 4LA SCOTLAND Tel: +44 1786 467 423 Fax: +44 1786 464 551 Web: http://www.cs.stir.ac.uk/~kjt
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page