|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: [email protected] |
| 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