University of Stirling (UNITED KINGDOM)
CADP (Construction and Analysis of Distributed Processes)
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.
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
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
Prof. Kenneth J. Turner
Department of Computing Science and Mathematics
University of Stirling
Stirling FK9 4LA
Tel: +44 1786 467 423
Fax: +44 1786 464 551
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies