Sylvain Rampacek

[Rampacek06] Sylvain RAMPACEK. Sémantique, interactions et langages de description des services web complexes. Thèse de doctorat, Reims, France, 10 Novembre 2006.

Résumé

Cette thèse de Doctorat s’articule autour des services web dont le processus métier est décrit en utilisant un langage de description comportementale tel que XLANG ou BPEL. Nous fournissons une méthode, des algorithmes et leurs implémentations permettant de modéliser sous forme de systèmes de transitions temporisées (TIOTS en temps discret et automates temporisés en temps dense) le comportement de ces services web. Pour cela, nous avons fixé une sémantique à l’aide des algèbres de processus temporisés nous permettant de décrire formellement le comportement, en terme d’actions, d’exceptions et d’évènements temporels, de chaque opérateur de ces langages de descriptions comportementales. Ces descriptions sont alors directement traduisibles dans le système de transitions temporisées choisi. Par la suite, grâce à notre relation d’interaction, nous pouvons détecter la non-ambiguïté d’un tel service ainsi modélisé, assurant l’interaction possible avec un client adapté dont nous fournissons alors le modèle. Nous avons également étendu notre approche à la possibilité de vérifier l’interaction des différents partenaires d’une chorégraphie, permettant ainsi de détecter une possible ambiguïté dans cette interaction.

Mots Clés

service web, modèle, comportement, vérification, sémantique, interaction, chorégraphie, TIOTS, automate temporisé, algèbre de processus temporisés.

Abstract

This PhD thesis is about web services, in which business process is described by using a behaviour description language, such as XLANG or BPEL. We give a method, algorithms and their implementations enable us to modelling in timed transition systems (TIOTS in discrete time and timed automaton in dense time) the behaviour of these web services. We give semantics with algebra of timed processes, enabling us to describe formally the behaviour, concerning actions, exceptions and timed events, of each operator of these behaviour description languages. These descriptions are directly translating in the given timed transition systems. In the next, with our interaction relation, we can detect the non ambiguity of this service, providing possible interaction with an adapted client that we produce the model. We extend our approach to the possibility to verify the interaction of different partners of a given choreography, enable us to detect a possible ambiguity in this interaction.

Keywords

web service, modelling, behavior, verification, semantics, interaction, choreography, TIOTS, timed automata, algebra of timed processes.

Version électronique