Researchers in software engineering proposed design method for distributed applications to construct a set of communicating system components from a global behavior. The joint behaviors of these components must precisely satisfy the specified global behavior. The next concern is to transform the constructed models of these components into executable business processes by ensuring the exchange of asynchronous messages among the generated business processes. The introduction of Service-Oriented Architecture (SOA) has helped to achieve this goal. SOA provides high flexibility in composing loosely-integrated services that can be used among business domains to carry out business transactions; this composition is known as service orchestration. Moreover, SOA supports Model Driven Architecture (MDA) such that services modeled as UML Activity Diagrams (AD) can be transformed into a set of Business Execution Language (BPEL) processes. Many researchers discussed the transformation of UML AD and the Business Process Modeling Notation (BPMN) into BPEL. However, they did not discuss the practical limitations that some of these transformations impose. This thesis addresses the imitations of the transformation from UML AD to BPEL processes using the IBM Rational Software Architect (RSA). We showed here that the tool is unable to create the correct BPEL artifacts from UML AD components in certain cases, for instance when the behavior includes the alternative for receiving single or concurrent messages, a weak loop, or certain choice activities. Furthermore, we provided novel solutions to the transformations in these cases in order to facilitate the transformation from UML AD to BPEL.

L’acceptation et l’utilisation des services Web en industrie se développent de par leursupport au développement d’application distribuées comme compositions d’entitéslogicielles plus simples appelées services. En complément à la vérification, le testpermet de vérifier la correction d’une implémentation binaire (code source nondisponible) par rapport à une spécification. Dans cette thèse, nous proposons uneapproche boîte-noire du test de conformité de compositions de services centralisées(orchestrations). Par rapport à l’état de l’art, nous développons une approchesymbolique de façon à éviter des problèmes d’explosion d’espace d’état dus à la largeutilisation de données XML dans les services Web. Cette approche est basée sur desmodèles symboliques (STS), l’exécution symbolique de ces modèles et l’utilisationd’un solveur SMT. De plus, nous proposons une approche de bout en bout, quiva de la spécification à l’aide d’un langage normalisé d’orchestration (ABPEL) etde la possible description d’objectifs de tests à la concrétisation et l’exécution enligne de cas de tests symboliques. Un point important est notre transformation demodèle entre ABPEL et les STS qui prend en compte les spécifications sémantiquesd’ABPEL. L’automatisation de notre approche est supportée par un ensemble d’outilsque nous avons développés. / Web services are gaining industry-wide acceptance and usage by fostering the developmentof distributed applications out of the composition of simpler entities calledservices. In complement to verification, testing allows one to check for the correctnessof a binary (no source code) service implementation with reference to a specification.In this thesis, we propose black box conformance testing approach for centralizedservice compositions (orchestrations). With reference to the state of the art, wedevelop a symbolic approach in order to avoid state space explosion issues due to theXML data being largely used in Web services. This approach is based on symbolicmodels (STS), symbolic execution, and the use of a satisfiability modulo theory(SMT) solver. Further, we propose a comprehensive end-to-end approach that goesfrom specification using a standard orchestration language (ABPEL), and the possibledescription of test purposes, to the online realization and execution of symbolic testcases against an implementation. A crucial point is a model transformation fromABPEL to STS that we have defined and that takes into account the peculiarities ofABPEL semantics. The automation of our approach is supported by a tool-chainthat we have developed.

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL.

L'acceptation et l'utilisation des services Web en industrie se développent de par leursupport au développement d'application distribuées comme compositions d'entitéslogicielles plus simples appelées services. En complément à la vérification, le testpermet de vérifier la correction d'une implémentation binaire (code source nondisponible) par rapport à une spécification. Dans cette thèse, nous proposons uneapproche boîte-noire du test de conformité de compositions de services centralisées(orchestrations). Par rapport à l'état de l'art, nous développons une approchesymbolique de façon à éviter des problèmes d'explosion d'espace d'état dus à la largeutilisation de données XML dans les services Web. Cette approche est basée sur desmodèles symboliques (STS), l'exécution symbolique de ces modèles et l'utilisationd'un solveur SMT. De plus, nous proposons une approche de bout en bout, quiva de la spécification à l'aide d'un langage normalisé d'orchestration (ABPEL) etde la possible description d'objectifs de tests à la concrétisation et l'exécution enligne de cas de tests symboliques. Un point important est notre transformation demodèle entre ABPEL et les STS qui prend en compte les spécifications sémantiquesd'ABPEL. L'automatisation de notre approche est supportée par un ensemble d'outilsque nous avons développés.

Cette thèse porte sur le diagnostic à base de modèles. Nous focalisons notre intérêt sur le diagnostic d'un ensemble interagissant de composants logiciels. L'originalité de ce travail se situe dans l'utilisation des Réseaux de Petri Colorés (RdPC) comme modèle de faute. L'utilisation des RdPC est originale et avantageuse à plusieurs titres. Premièrement, Les RdPC permettent la représentation des données, dans notre cas ça nous permet de manipuler les données de manière symbolique même si leur domaine de valeurs est infini (seul le statut des données est représenté par des jetons colorés : rouge pour fautif, noir pour correct et étoile pour inconnu). Deuxièmement, chaque transition en RdPC peut avoir plusieurs modalités de franchissement, nous avons donc défini pour chaque activité deux modalités de transition, fautif et correct, auxquelles on a associé des fonctions de propagation de couleur. Finalement, La sémantique RdPC porte de manière implicite la notion d'ordre partiel des observations. La contribution principale de cette thèse consiste à réduire le problème de diagnostic à la résolution d' un système d'inéquation algébrique en se fondant sur l'équation fondamentale de la dynamique des RdPs. La résolution de ce système d'inéquation permet de calculer le diagnostic sans dépliage de la trajectoire même dans les cas d'itération d'activités et ceci sans perte de la précision du diagnostic. Nous avons également, en se fondant sur la notion de sous-réseaux fonctionnels, proposé une version décentralisée de la résolution du système d'inéquation. La dimension applicative de cette thèse concerne le diagnostic d'orchestration de services Web. Une traduction du langage d'orchestration BPEL en RdPC a été donné ainsi qu'une application détaillée sur un scénario.

Les Web Services sont aujourd'hui à la base de nombreuses applications de commerce électronique. Aujourd'hui les solutions de sécurité qui sont proposées pour les Web-Services permettent de protéger en confidentialité et en intégrité les communications entre les Web-Services et de contrôler l'accès aux Web-Services. Cependant, le plus souvent, les clients utilisent ces applications sans en connaître le fonctionnement interne. De ce fait, ils n'ont aucune connaissance sur l'usage de leurs données qui est effectué à l'intérieur d'une application. BPEL (Business Process Execution Language) est un langage de programmation permettant d'orchestrer des Web-Services au sein d'une architecture orientée services. Une des fonctionnalités des architectures orientées services est la découverte dynamique des services effectivement utilisés au cours de l'exécution d'une orchestration. De ce fait, l'utilisateur d'un programme BPEL ne peut connaitre avant l'exécution comment et par qui les données qu'il va fournir seront utilisées. Dans le cadre de cette thèse, nous proposons un modèle de politique de contrôle de flux d'information adapté aux architectures orientées services et en particulier aux orchestrations de services. Ce modèle offre aux utilisateurs la possibilité de spécifier des contraintes sur l'usage qui est fait de leurs données personnelles. Les politiques de contrôle de flux d'information définies suivant ce modèle sont définies au cours de l'exécution par l'utilisateur d'une orchestration de services. Les aspects dynamiques des Web-Services conduisent, en effet, à des situations où la politique peut empêcher l'exécution nominale de l'orchestration (par exemple lorsqu'il est fait usage d'un service que l'utilisateur ne connaissait pas avant l'exécution). A cet effet, nous proposons à l'utilisateur d'autoriser dynamiquement des modifications de la politique de contrôle de flux d'information. Afin de lui permettre d'effectuer cette modification, nous proposons dans le cadre de cette thèse un mécanisme permettant à l'utilisateur de disposer d'un maximum d'informations sur l'usage qui est fait de ses données et qui conduit à une violation de la politique de contrôle de flux d'information. Nous avons ensuite appliqué cette approche au langage d'orchestration BPEL. Nous avons en particulier présenté les principaux flux d'information qui interviennent dans ce langage. Nous avons enfin proposé une implémentation de ces mécanismes de contrôle de flux d'information en modifiant un orchestrateur BPEL existant.

Today, Peer-to-peer (P2P) computing and Web Services play an important role in networking and computing. P2P computing, that aims addressing all the resources in a network and sharing them, is an old paradigm that gains importance nowadays with the advent of popular file sharing and instant messaging applications. On the other hand, a Web service is a software system that has an interface allowing applications to interact with other applications through Internet or intranet. Providing methods for publishing and discovering Web services from which mobile devices can facilitate in a P2P environment enables exploitation of P2P and Web service technologies efficiently by mobile devices. This also extends the range of devices that facilitate P2P and Web services technologies from servers and desktop computers to personal digital assistants (PDAs) and mobile phones. In this thesis, an architecture that enables publishing and discovering Web services for mobile clients that are inter-connected in a P2P environment is introduced. Key issues in this architecture are allowing mobile devices to join in a P2P network group, publishing Web services and discovering these services in P2P network. Invoking Web services that are published and discovered is another key issue in this architecture. The architecture introduced exploits P2P and Web services standards using various tools for mobile devices. For the purpose of organizing a P2P environment, JXTA protocols and services are used. WSDL is used for describing Web services. JXTA advertisements help in publication and discovery of Web services / and BPEL enables composition, deployment and execution of Web services. The architecture introduced within the scope of this thesis combines all these standards with tools that enable use of these standards on mobile devices. The work done in this thesis is realized as a part of Artemis, a project funded by European Commission for providing interoperability of medical information systems.

Die Softwareentwicklung ist seit den Anfängen der Informatik stetig effizienter geworden. Beispielsweise wird heute neue Software fast schon vollautomatisch entwickelt. Neben der stark geförderten Wiederverwendung von Systemkomponenten und anderen mehr oder weniger verbreiteten Methoden, welche die Produktivität oder auch Softwarequalität verbessern sollen1, ist die modellgetriebene Softwareentwicklung ein sehr effizientes und weit verbreitetes Konzept, qualitativ hochwertige Softwaresysteme zu entwickeln. Bei der modellgetriebenen Softwareentwicklung spielen die Modelle der abzubildenden Realitätsausschnitte eine wichtigere Rolle als in der klassischen Softwareentwicklung. Hier werden die erstellten Modelle dazu verwendet Code, Dokumentationen oder andere Artefakte mittels Transformationen zu erzeugen. Beispielsweise können so auch Modelle anderer Modellierungssprachen aus den bestehenden Modellen erzeugt werden.

Currently, there are many software applications handling planning, scheduling, material management, invoicing, workflow management within an organization. However, companies need to plan across a wider span of activities and need to collaborate with their partners to optimize the &#039 / &#039 / overall&#039 / &#039 / profitability. This requires collaborative planning within a supply chain and exchange of planning data. Collaborative Planning, Forecast and Replenishment (CPFR) is one of the most prominent initiatives on Collaborative Planning. However, CPFR only provides guidelines, but does not mandate any technology for the definition and execution of planning process. Therefore, companies have difficulties to define and deploy CPFR solutions and there is a need for a Service Oriented, Open Platform for the definition and execution of collaborative planning processes involving many supply chain tiers. In this work, first of all, the building blocks of the planning process have been defined as machine processable definitions in OASIS ebXML Business Specification Language (ebBP). CPFR Designer Tool developed provides the users to visually create CPFR Processes in ebBP and to convert this ebBP process definition automatically to an executable business process using OASIS Business Process Execution Language (WS-BPEL). In this way, the supply chain enterprises are able to create customized CPFR processes which are in integration with the underlying intra-enterprise planning processes. Moreover, in the thesis, a CPFR Process Execution Environment is prepared where the generated CPFR Process can be executed. The work presented in this thesis is realized as a part of IST-213031 iSURF project funded by European Commission under ICT FP7.

Cette thèse s'intéresse à l'orchestration de services répartie, résultat (1) d'une approche explicite de découpage d'une orchestration en sous-orchestrations localisées sur des sites physiques distants à des fins de protection de données par exemple, ou (2) d'une approche constructive issue du regroupement d'orchestrations existantes potentiellement hétérogènes, afin de constituer une orchestration globale mais répartie. Les orchestrations de services reflètent des processus métiers, souvent de longue durée, et qui doivent donc pouvoir être adaptables dynamiquement à l'exécution. Cette thèse propose un support d'exécution pour des orchestrations réparties, hétérogènes, dynamiquement reconfigurables, et permettant une administration globale. Une orchestration de services peut être abordée selon ses deux dimensions : temporelle qui reflète l'enchainement des services dans le temps, spatiale qui reflète les services que l'orchestration a besoin d'invoquer afin de s'exécuter. Nous proposons ainsi un nouveau modèle à composants pour les applications orientées services, inspiré en partie de SCA et de SCA/BPEL, mais permettant de représenter ces deux dimensions. Notre approche se fonde sur un modèle de composants logiciels répartis et dynamiquement reconfigurables, et hérite donc des qualités de répartition et de reconfiguration dynamique. Nous décrivons une mise en oeuvre au dessus de l'implémentation du modèle "Grid Component Model" sur la plateforme de programmation répartie à objets actifs "ProActive". Nous validons notre approche expérimentalement via une application à services d'installation et d'administration d'un parc de passerelles basées sur OSGi.