Ces dernières années ont vu l’émergence d’architectures orientées services (SOA) conçues pour faciliter la création, l’exposition, l’interconnexion et la réutilisation d’applications à base de services. Les services Web sont la réalisation la plus importante de cette architecture SOA. Ce sont des applications auto descriptives et modulaires fournissant un modèle simple de programmation et de déploiement d’applications. La composition de services Web, en particulier l’orchestration, est au coeur de l’ingénierie à base de services (SOC pour Service Oriented Computing) puisque elle supporte la construction de nouveaux services composés à partir de services de base. De son côté, WS-BPEL (ou BPEL) s’est imposé depuis 2005 comme le langage standard d’orchestration de services Web. Cette thèse de Doctorat s’articule autour du test fonctionnel de l’orchestration de services décrite en langage BPEL, qui consiste à établir la conformité de l’implantation d’un service composé par rapport à sa spécification. Nos activités de recherche ont été motivées par les caractéristiques spécifiques de la composition de services surtout celle décrite en BPEL, et par la nécessité d’automatisation des tests. L’objectif de cette thèse est double : d’une part, proposer une modélisation formelle de l’orchestration de services, et d’autre part, proposer une méthode de test complète de l’orchestration de services, allant de la modélisation formelle de l’orchestration à l’exécution des tests, incluant la génération automatique de cas de test. Notre modèle formel (appelé WS-TEFSM) permet de décrire une grande partie de BPEL et prend en considération les propriétés temporelles de la composition de service. La modélisation formelle est la première phase de notre approche de test. Par conséquent, nous utilisons le modèle formel résultant pour la génération de cas de test satisfaisant un ensemble d’objectifs de test. L’automatisation de la génération de cas de test a été mise en oeuvre par l’implémentation d’une stratégie efficace d’exploration partielle de l’espace d’états (i.e. Hit-Or-Jump) dans le simulateur IF. Pour se focaliser seulement sur les erreurs potentielles du service orchestrateur (service composé), nous proposons une approche de test boîte grise consistant à simuler les services partenaires de cet orchestrateur. Nous avons abordé ces problématiques à la fois d’un point de vue théorique et pratique. En plus de la proposition d’une modélisation formelle de l’orchestration de services et d’un algorithme de génération de cas de test temporisés, nous avons implémenté ces deux concepts en développant deux prototypes. BPEL2IF permet de transformer une orchestration de services décrite en BPEL en une spécification formelle à base d’automates temporisés (spécification IF). TestGen-IF permet de dériver automatiquement des cas de test temporisés. Enfin, pour valider notre démarche, nous avons appliqué notre approche de test à des cas d’études de taille réelle. / Last years have seen the emergence of the service oriented architecture (SOA) designed to facilitate the creation, the publication, the networking and the reuse of applications based on services. Web services are the most important realization of the SOA architecture. They are self descriptive and modular entities which provide a simple model of programming and application deployment. Web services composition, especially orchestration, is at the heart of service oriented computing (SOC), since it supports the construction of new composite services out of basic services. WS-BPEL (BPEL for short) has emerged since 2005 as the standard language for Web service orchestration. This PhD thesis focuses on functional testing of service orchestrations described in BPEL, which aims to establish the conformance of a composite service implementation to its specification. Our research activities have been motivated by specific features of the BPEL composition, and the need for test automation. The objective of this thesis is twofold : on the one hand, to propose a formal modeling of service orchestration, and on the other hand, to propose a comprehensive testing approach for orchestrations, ranging from orchestration modeling to tests execution, including automatic test case generation. Compared to existing work, our formal model covers a large subset of BPEL constructs and focuses on the temporal properties of the composition. The formal model is a first step of our testing approach. Afterwards, we use the model to generate the test cases according to test purposes. We automate the test generation by implementing an efficient state space search strategy inside an open-source simulator, i.e. the IF simulator. In our case, to focus on the potential errors of the orchestrator, we propose a gray box approach which consists on the simulation of the partners of this orchestrator. We have addressed these issues both from a theoretical and practical perspective. Therefore, besides proposing expressive orchestration models and test case generation algorithm, we have developed prototypes (BPEL2IF and TestGen-IF) as a proof of concepts. BPEL2IF transforms a BPEL orchestration into a formal specification based on timed automata (IF specification). TestGen- IF generates automatically timed test cases. Moreover, to validate our proposal, we have applied our testing approach on real size case studies.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

La modélisation dans le domaine de l'agro-écologie est importante car elle permet de mieux comprendre les interactions entre l'environnement et les activités humaines. Des travaux basés sur la simulation ont été développés depuis des années. Cependant, non seulement ces outils restent difficiles à utiliser par les utilisateurs non experts, mais aussi le coût des modèles rend leur utilisation difficile à case de la complexité élevée en cas d'application réelle. Nous proposons une approche qui consiste à représenter le système étudié dans un formalisme de système à événements discrets qui est bien adapté quand la dynamique du système est liée à des interactions entre les entités concernés. Ceci permet de profiter l'efficacité du model-checking pour étudier le comportement du système modélisé et d'utiliser la synthèse de contrôleur pour générer automatiquement des stratégies optimales. Nous présentons deux contributions dans cette thèse. La première contribution concerne le projet EcoMata. Cette modélisation qualitative en automates temporisés pour un réseau trophique marin de type proie-prédateur permet d'analyser l'écosystème à l'aide de model-checking sans avoir à faire des simulations. Des scénarios de requête prédéfinis ont été développés dans un langage naturel pour que les utilisateurs non expert puissent faire des requêtes sur les réseaux trophiques sans avoir des connaissances sur la langage TCTL. Nous avons amélioré la génération automatique d'automates temporisés à partir d'une description des équation Lotka-Votera. Nous avons aussi proposé une approche de synthèse de contrôleur pour générer automatiquement des stratégies optimales de gestion de pêche. Le prototype logiciel EcoMata implémente l'ensemble des propositions incluant la recherche de stratégies optimales. Dans la seconde contribution, nous proposons une modélisation hybride en automates temporisés d'une exploitation de pâturage. Cette modélisation hybride combine un modèle numérique de la croissance d'herbe et un modèle qualitatif des activités de pâturage. Une structure hiérarchique organise les modèles dans quatre couches: la couche biologique, la couche activité, la couche décisionnelle et la couche d'horloge. Nous proposons quatre méthodes pour générer des stratégies optimales des activités de pâturage. La première méthode est appliquée à la recherche de stratégies optimales de la mise au pâturage. Trois méthodes sont dédiées à la recherche de stratégies optimales de la fertilisation. Une d'entre elles utilise la synthèse de contrôleur alors que les deux autres combinent la synthèse de contrôleur et l'apprentissage supervisé pour générer des stratégies génériques par type d'exploitation. Un prototype logiciel PaturMata a été développé implémentant cette modélisation, permettant aux utilisateurs de simuler des scénarios de pâturage et rechercher des stratégies optimales de mise au pâturage. / The modeling in the domain of agro-ecology is important since it helps us to better understand the interactiosn between the environment and the human activities. Some research works based on simulation has been carried out during the recent years. Mainwhile, not only these simulation tools are difficult to use by the non expert users, but also the high complexity of models makes interactive uses impossible. We propose an approch in which we represent the system to be studied in a discret event system formalism. This kind of representation benefits the efficiency of model-checking and makes it possible to use controller synthesis to generate strategies. We present two contributions in this thesis. The first one concerns the project EcoMata. This project proposes a qualitative modelling which represents a marine prey-predator type food chain in timed automata. Predifined query patterns in natural langurage are also proposed which allow users to investigate easiy the food chain. We have improved the efficiency of the algorithm of timed automata generation and also developped a strategy synthesis method to generate best fishing management strategy. The prototype software EcoMata implements all these propositions including the best strategy synthesis. In the second contribution, we propose a hybrid modelling which represents grazing activities in timed automata. This hybrid modelling combines a numerical grass model and a qualitative grazing model. These sub models are organized in a hierarchical struture of four layers: the biological layer, the activity layer, the decision layer and the clock. We propose four methods to generate best grazing management strategy. One of these methods is applied to the movement of herd. The other three methods are applied to fertilization among which one of them use controller synthesis on timed automata and the other two combine controller synthesis and machine learning to generate generic strategy for a exploitation type. A prototype software PaturMata has been developped which implements this modelling method and the generation of the best strategy of herd movement.

Un automate temporisé est un automate augmenté avec plusieurs horloges qui mesurent le passage de temps et peuvent conditionner la modification de l'état du système. Les automates temporisés ont été introduits en tant que modèle formel pour les systèmes temps-réel, en espérant que leur rôle dans la vérification de tels systèmes sera similaire au rôle des automates finis dans la recherche systématique des erreurs de conception de systèmes non-temporisés. Dans notre thèse nous étudions plusieurs questions théoriques liés aux automates temporisés et aux langages temporisés. Dans une première partie nous étudions une sous-classe simple d'automates temporisés à une seule horloge qui est remise à zéro pendant chaque transition. Nous montrons que cette sous-classe supporte des résultats similaires à la théorie classique des automates finis: des théorèmes de Kleene, de Myhill-Nerode et de fermeture par complémentation. La deuxième et principale partie de la thèse est motivée par les expressions régulières temporisés de Asarin, Caspi et Maler. Depuis leur introduction, on sait qu'il faut employer l'intersection dans les expressions régulières pour que leur expressivité soit égale aux automates temporisés. Nous poursuivons alors une approche alternative en utilisant des parenthèses colorées pour définir les contraintes temporelles sur une séquence d'événements. Cette idée aboutit à une représentation alternative des langage des automates temporisés, basée sur une nouvelle classe de langages formels que nous appelons . Nous développons alors la théorie des expressions régulières sur les regminos et nous montrons que le problème de sémantique vide est indécidable en cas général, et décidable pour une sous-classe large de langages. L'application de ces résultats nous amène à des nouvelles structures de données et à des algorithmes pour le problème du langage vide dans les automates temporisés et les expressions régulières.

Les travaux de recherche présentés dans cette thèse proposent une méthodologie de synthèse de la commande des systèmes à événements discrets temporisés permettant de calculer l'ensemble de toutes les lois de commande telles que le fonctionnement du système respecte les spécifications imposées par le cahier des charges. Notre approche associe la capacité de modélisation de l'outil réseau de Petri T-temporel à la puissance d'analyse des automates temporisés. Dans un premier temps, le système à commander est modélisé par un réseau de Petri T-temporel. Ensuite on construit l'automate temporisé qui modélise le comportement de ce réseau de Petri T-temporel. Les comportements non-désirés sont modélisés par des sommets interdits. La synthèse de la commande est basée sur des techniques d'analyse d'atteignabilité spécifiques aux automates temporisés. La méthode proposée consiste à calculer des nouvelles gardes des transitions de l'automate telles que les sommets interdits ne soient jamais atteints. L'approche de synthèse de la commande présenté dans cette thèse s'adresse aux systèmes à événements discrets temporisés modélisés par des réseaux de Petri T-temporels bornés avec des contraintes temporelles spécifiées par des nombres rationnels.

Le but de la thèse est de développer une nouvelle approche de surveillance des systèmes à événements discrets. La méthode proposée est basée sur la surveillance du temps de service en utilisant l'automate temporisé comme outil de modélisation.<br />Partant d'un système commandé, le premier objectif est la surveillance des différentes activités de ce système afin d'améliorer sa disponibilité. Ceci se traduit par la minimisation du nombre d'arrêts qui pénalisent la production, en suivant en temps réel, l'état de fonctionnement des différents capteurs du système. Ainsi pour chaque tâche, la surveillance du temps écoulé entre deux événements (l'instant où la commande a donné l'ordre de démarrer une tâche et l'instant où le capteur indique la fin d'exécution de la tâche) permet de détecter au plutôt d'éventuelles défaillances. La deuxième phase correspond au diagnostic qui consiste en la détermination des causes du problème observé.<br />Jusqu'à présent les approches de surveillance utilisent un modèle de référence basé sur la connaissance à priori de toutes les situations interdites du système. Le modèle de surveillance proposé présente un réel avantage. En effet, la détection d'éventuelles défaillances ne nécessite pas une liste exhaustive de toutes les défaillances possibles du système. En fonction de la catégorie du système de production et de la nature des tâches à surveiller nous introduisons une tolérance sur la durée de la tâche à surveiller. Ainsi, la notion de fonctionnement en ‘ mode dégradé' est introduite. Au-delà de cette tolérance, le système sera effectivement dans un état de ‘défaillance'. Différents exemples illustrent la démarche proposée. Ils permettent de montrer la puissance d'une telle approche. De plus, un algorithme permettant le calcul du seuil optimal de tolérance est proposé, ainsi que l'évaluation des performances du système de surveillance.

De nombreux sytèmes critiques comportent des aspects temporisés, où interviennent de manière cruciale des contraintes quantitatives sur les délais séparant certaines actions. Un automate programmable industriel (API) constitue un composant fondamental d'un système souvent critique destiné à réagir et à communiquer en temps réel avec son environnement. Ma thèse se situe dans le contexte de la vérification de propriétés temporisées des APIS. Plus précisement, on propose une sémantique formelle à base d'automates temporisés pour la modélisation d'une sous classe de programmes Ladder comportant des blocs TON. On fournie une logique temporisée dont la sémantique permet de considérer seulement les événements "signifcatifs" (c'est à dire les événements qui durent suffisamment longtemps). On propose deux sémantiques différentes pour cette logique: sémantique "locale" et sémantique "globale". Pour la sémantique "locale", on a obtenu plusieurs résultats d'expressivité et grâce à une nouvelle relation d'équivalence, on montre que son model checking reste décidable sans modifier la complexité théorique. En revanche, pour la sémantique "globale", le model checking devient indécidable.

La modélisation dans le domaine de l'agro-écologie est importante car elle permet de mieux comprendre les interactions entre l'environnement et les activités humaines. Des travaux basés sur la simulation ont été développés depuis des années. Cependant, non seulement ces outils restent difficiles à utiliser par les utilisateurs non experts, mais aussi le coût des modèles rend leur utilisation difficile à case de la complexité élevée en cas d'application réelle. Nous proposons une approche qui consiste à représenter le système étudié dans un formalisme de système à événements discrets qui est bien adapté quand la dynamique du système est liée à des interactions entre les entités concernés. Ceci permet de profiter l'efficacité du model-checking pour étudier le comportement du système modélisé et d'utiliser la synthèse de contrôleur pour générer automatiquement des stratégies optimales. Nous présentons deux contributions dans cette thèse. La première contribution concerne le projet EcoMata. Cette modélisation qualitative en automates temporisés pour un réseau trophique marin de type proie-prédateur permet d'analyser l'écosystème à l'aide de model-checking sans avoir à faire des simulations. Des scénarios de requête prédéfinis ont été développés dans un langage naturel pour que les utilisateurs non expert puissent faire des requêtes sur les réseaux trophiques sans avoir des connaissances sur la langage TCTL. Nous avons amélioré la génération automatique d'automates temporisés à partir d'une description des équation Lotka-Votera. Nous avons aussi proposé une approche de synthèse de contrôleur pour générer automatiquement des stratégies optimales de gestion de pêche. Le prototype logiciel EcoMata implémente l'ensemble des propositions incluant la recherche de stratégies optimales. Dans la seconde contribution, nous proposons une modélisation hybride en automates temporisés d'une exploitation de pâturage. Cette modélisation hybride combine un modèle numérique de la croissance d'herbe et un modèle qualitatif des activités de pâturage. Une structure hiérarchique organise les modèles dans quatre couches: la couche biologique, la couche activité, la couche décisionnelle et la couche d'horloge. Nous proposons quatre méthodes pour générer des stratégies optimales des activités de pâturage. La première méthode est appliquée à la recherche de stratégies optimales de la mise au pâturage. Trois méthodes sont dédiées à la recherche de stratégies optimales de la fertilisation. Une d'entre elles utilise la synthèse de contrôleur alors que les deux autres combinent la synthèse de contrôleur et l'apprentissage supervisé pour générer des stratégies génériques par type d'exploitation. Un prototype logiciel PaturMata a été développé implémentant cette modélisation, permettant aux utilisateurs de simuler des scénarios de pâturage et rechercher des stratégies optimales de mise au pâturage.

La vérification en ligne de spécifications formelles permet de créer des détecteurs d'erreur dont le pouvoir de détection dépend en grande partie du formalisme vérifié à l'exécution. Plus le formalisme est puissant plus la séparation entre les exécutions correctes et erronées peut être précise. Cependant, l'utilisation des vérifieurs en-ligne dans le but de détecter des erreurs est entravée par deux problèmes récurrents : le coût à l'exécution de ces vérifications, et le flou entourant les propriétés sémantiques exactes des signaux d'erreur ainsi générés. L'objectif de cette thèse est de clarifier les conditions d'utilisation de tels détecteurs dans le cadre d'applications « temps réel » critiques. Dans ce but, nous avons donné l'interprétation formelle de la notion d'erreur comportementale « temps réel». Nous définissions la propriété de détection « au plus tôt » qui permet de d'identifier la classe des détecteurs qui optimisent la latence de détection. Pour illustrer cette classe de détecteurs, nous proposons un prototype qui vérifie un comportement décrit par un automate temporisé. La propriété de détection au plus tôt est atteinte en raisonnant sur l'abstraction temporelle de l'automate et non sur l'automate lui-même. Nos contributions se déclinent dans trois domaines, la formalisation de la détection au plus tôt, sa traduction pour la synthèse de détecteurs d'erreur à partir d'automate temporisés, puis le déploiement concret de ces détecteurs sur une plate-forme de développement temps réel, Xenomai. / Runtime verification of formal specifications provides the means to generate error detectors with detection capabilities depending mostly on the kind of formalism considered. The stronger the formalism is the easier the speration between correct and erroneous execution is. Nevertheless, two recurring issues have to be considered before using such error detection mechanisms. First, the cost, at run-time, of such error detector has to be assessed. Then, we have to ensure that the execution of such detectors has a well defined semantics. This thesis aims at better understanding the conditions of use of such detectors within critical real-time software application. Given formal behavioural specification, we defined the notion of "behavioural error". Then, we identify the class of early detectors that optimize the detection latency between the occurence of such errors and their signalling. The whole generation process has been implemented for specifications provided as timed automata. The prototype achieves early error detection thanks to a preprocessing of the automaton to generate its temporal abstraction. Our contributions are threefold : formalisation of early detection, algorithms for timed automata run-time verification, and prototyping of such detectors on a real-time kernel, Xenomai.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.