Database of Case Studies Achieved Using CADP

Specification and Analysis of a Web Service for GPS Navigation

Organisation: INRIA Rhône-Alpes (France)
Université de Bourgogne (France)

Method: ATP (Algebra of Times Processes)
MCL (Model Checking Language)

Tools used: CADP (Construction and Analysis of Distributed Processes)
WSMod

Domain: Web Services.

Period: 2008

Size: 535 states and 1473 transitions.

Description: Service Oriented Architecture (SOA) is a state-of-the-art methodology for developing information systems by structuring them in terms of services, which can be distributed and composed over a network infrastructure to form complex business processes. Web services are a useful basis for implementing business processes, either by wrapping existing software or by creating new functionalities as combinations of simpler ones. BPEL (Business Process Execution Language) is a standardized language of wide industrial usage for describing abstract business processes and detailed Web services. It allows to capture both the behavioral aspects (concurrency and communication) and the timing aspects (duration of activities) of Web services.

A tool-supported approach is proposed for the formal modeling and analysis of business processes and Web services described in BPEL. The approach consists of the following ingredients: the definition of a formal semantics of BPEL using rules of ATP (Algebra of Timed Processes), taking into account the discrete-timing aspects; the automated generation of LTS models from the BPEL specifications using an exhaustive simulation based on the formal semantics rules, implemented in the WSMod tool; and the analysis of the resulting models by using CADP.

The approach is illustrated by the design and discrete-time analysis of a Web service for GPS navigation. The purpose of this Web service is to compute itineraries from a position to a destination fixed by a user (client of the service). In addition to the requested itinerary, the user can also obtain: pictures of the travel (taken from the air), the global map of the itinerary, and various kinds of information (about traffic, radar stations, point of interest (POI), etc). At last, the user can configure the subscription to the various kinds of information, as well as some parameters of the travel (e.g., to take motorway or not, to deviate towards a POI, etc.). The behavior of the GPS Web service consists of two main phases, described in the sequel: the initialization phase (login, setting of the initial position and destination) and the main loop phase (management of the itinerary, modification of the parameters, etc.).

Starting from a BPEL description of the Web service, the corresponding discrete-time LTS (dtLTS) was generated using the WSMod tool, for timeout values ranging from 1 to 60 seconds. The behaviour of the GPS Web service was subsequently analyzed by performing discrete-time model checking on the dtLTS for a timeout of 50 seconds, using the EVALUATOR tool of CADP. Eight temporal properties stating the correct behaviour of the Web service were successfully verified.

Conclusions: The conjunction of concurrency and timing constraints makes business processes complex and requires a careful design in order to avoid information losses and to obtain a satisfactory quality of service. In this context, formal modeling and analysis techniques available from the domain of concurrent systems allow to improve the quality of the design process and to reduce the development costs by detecting errors as soon as possible during the business process life cycle.

Publications: [Mateescu-Rampacek-08-a] Radu Mateescu and Sylvain Rampacek. "Formal Modeling and Discrete-Time Analysis of BPEL Web Services". In Joseph Barjis, Murali Mohan Narasipuram, and Peter Rittgen, editors, Proceedings of the 4th International Workshop on Enterprise and Organizational Modeling and Simulation EOMAS'08 (Montpellier, France), Lecture Notes in Business Information Processing, vol. 10, pp. 179-193, June 2008.
Available on-line from http://cadp.inria.fr/publications/Mateescu-Rampacek-08-a.html
Contact:
Sylvain Rampacek
IUT de Dijon - Département Informatique - Bureau 12
Université de Bourgogne
Boulevard Docteur Petitjean - BP 17867
F-21078 Dijon Cedex
FRANCE
Tel: +33 (0)3 80 39 65 67
Email: Sylvain.Rampacek@u-bourgogne.fr



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Tue Sep 8 18:14:48 2015.


Back to the CADP case studies page