Return to search

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

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 and bottom-up approaches. It consists in analyzing the 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 the 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 the testing process. Our framework is fully implemented in our toolchains, which can be downloaded or used online at address: http://schora.lri.fr.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00961450
Date31 October 2013
CreatorsNguyễn, Huu Nghia (Hữu Nghĩa)
PublisherUniversité Paris Sud - Paris XI
Source SetsCCSD theses-EN-ligne, France
LanguageEnglish
Detected LanguageEnglish
TypePhD thesis

Page generated in 0.0021 seconds