Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Ph.D de

Group : Large-scale Heterogeneous DAta and Knowledge

A symbolic approach for the verification and the testing of service choreographies

Starts on 24/11/2009
Advisor : ZAIDI, Fatiha

Funding :
Affiliation : Université Paris-Saclay
Laboratory : LRI

Defended on 31/10/2013, committee :
- Manuel Núñez, Professeur, Universidad Complutense de Madrid, Espagne
- Gwen Salaün, Mdc HDR, Grenoble Inp, Inria, France

- Philippe Dague, Professeur, Université Paris-Sud, France
- Gianluigi Zavattaro, Professeur, Università di Bologna, Italy

Directeurs de thèse:
- Pascal Poizat, Professeur, Université Paris Ouest Nanterre la Défense, France
- Fatia Zaïdi, Mdc HDR, Université Paris Sud , France

Research activities :
   - Formal Model-Based Testing

Abstract :
Service-oriented engineering is an emerging software development paradigm for distributed collaborative applications. Such an application is made up of several entities abstracted as services, each of them being for example a Web application, a Web service, or even a human. The services can be developed independently and are composed to achieve common requirements through interactions among them. Service choreographies define such requirements from a global perspective, based on interactions among a set of participants.

This thesis aims to formalize the problems and attempts to develop a framework by which service choreographies can be developed correctly for both top-down or bottom-up approaches. It consists in analyzing relation between a choreography specification and a choreography implementation at both model level and real implementation level. Particularly, it concerns the composition/decomposition service design, the verification, and the testing of choreography implementation.

The first key point of our framework is to support value-passing among services by using symbolic technique and SMT solver. It overcomes false negatives or state space explosion issues due by abstracting or limiting data domain of value-passing in existing approaches.

The second key point is the black-box passive testing of choreography implementation. It does not require neither to access to source codes nor to make the implementation unavailable during testing process.

Our framework is fully implemented in our toolchains which can be downloaded or used online at address