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

Ph.D
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-Sud
Laboratory : LRI

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

Examinateurs:
- 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 http://schora.lri.fr.

Ph.D. dissertations & Faculty habilitations
APPRENTISSAGE ET OPTIMISATION SUR LES GRAPHES


ANALYSE DE DONNéES MULTI-MODALES POUR LES PATHOLOGIES COMPLEXES PAR LA CONCEPTION ET L’IMPLéMENTATION DE PROTOCOLES REPRODUCTIBLES ET RéUTILISABLES


DESIGNING INTERACTIVE TOOLS FOR CREATORS AND CREATIVE WORK
Creative work has been at the core of research in Human-Computer Interaction (HCI). I describe the results of a series of studies that look at how creators work, where creators include artists with years of professional practice, as well as learners, or novices and casual makers. My research focuses on three creation activities: drawing, physical modeling, and music composition. For these activities, I examine how artists switch between representations and how these representations evolve throughout their creative process, from early sketches to fine-grained forms or structured vocabularies. I present interactive systems that enrich their workflow (i) by extending their computer tools with physical user interfaces, or (ii) by making physical materials interactive. I also argue that sketch-based representations can allow for user interfaces that are more personal and less rigid. My presentation will reflect on lessons and limitations of this work and discuss challenges for future design-support tools.