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.

Depuis le début des années 90, les automates temporisés et les langages temporisés ont été largement utilisés pour modéliser et vérifier les systèmes temps réels. Ces langages ont été aussi été largement étudiés d'un point de vue théorique. Plus récemment Asarin et Degorre ont introduit les notions de volume et d'entropie des langages temporisés pour quantifier la taille de ces langages et l'information que ses éléments contiennent. Dans cette thèse nous construisons de nouveaux développements à cette théorie (que nous appelons volumétrie des langages temporisés) et l'appliquons a plusieurs problèmes apparaissant dans divers domaine de recherche tel que la théorie de l'information, la vérification, la combinatoire énumérative. Entre autre nous (i) développons une théorie de la dynamique symbolique temporisée~; (ii) caractérisons une dichotomie entre automate temporisé se comportant bien ou mal~; (iii) définissons pour un automate temporisé donné, un processus stochastique d'entropie maximale le moins biaisé possible~; (iv) développons une version temporisé de la théorie des codes sur canal contraint (v) énumérons et générons aléatoirement des permutations dans une certaine classe / Since early 90s, timed automata and timed languages are extensively used for modelling and verification of real-time systems, and thoroughly explored from a theoretical standpoint. Recently Asarin and Degorre introduced the notions of volume and entropy of timed languages to quantify the size of these languages and the information content of their elements. In this thesis we build new developments of this theory (called by us volumetry of timed languages) and apply it to several problems occurring in various domains of theoretical computer science such as verification, enumerative combinatorics or information theory. Among other we (i) develop a theory of timed symbolic dynamics; (ii) characterize a dichotomy between bad behaving and well behaving timed automata; (iii) define a least biased stochastic process for a timed automaton; (iv) develop a timed theory of constrained channel coding; (v)count and generate randomly and uniformly permutations in certain classes

La vérification et la validation des composants logiciels des systèmes temps réel est un des enjeuxmajeurs pour le développement de systèmes automatisés. Les modèles de tels systèmes doiventêtre vérifiés, et la conformité de leur implémentation par rapport à leur modèle doit être validée. Nous nous plaçons dans le cadre des systèmes récursifs temps réels modélisables par des automates à pile temporisés avec deadlines (TPAIO). Les deadlines imposent des conditions de progression du temps. L’objectif de cette thèse est de proposer des méthodes de génération de tests pour les TPAIO.Nos contributions sont les suivantes. Premièrement, une relation de conformité pour les TPAIO est introduite. Deuxièmement, une méthode polynomiale de génération de tests à partir d’un TPAIO déterministe avec deadline lazy est définie. Elle consiste à définir un algorithme de calcul d’un automate temporisé d’accessibilité incomplet en respectant les contraintes de pile. Cette méthode est incomplète. L’incomplétude n'étant pas un problème car l’activité de test est par essence incomplète. Troisièmement, nous définissons une méthode générant des cas de tests à partir d’un TPAIO déterministe avec sorties seulement et deadline delayable seulement. Elle d’applique aux abstractions de programmes récursifs temporisés. Elle consiste à générer des cas de tests en calculant un testeur sur-approximé. Finalement, nous avons proposé une généralisation du processus de génération de tests à partir d’un TPAIO général avec entrées/sorties et avec deadlines quelconques. La capacité de cette dernière méthode à détecter des implémentations non conformes est évaluée par une technique de mutation. / The verification and validation of software components for real-time systems is a major challenge for the development of automated systems. The models of such systems must be verified and the conformance of their implementation w.r.t their model must be validated. Our framework is that of real-time recursive systems modelled by timed pushdown automata with deadlines (TPAIO). The deadlines impose time progress conditions. The objective of this thesis is to propose test generation methods from TPAIO.Our contributions are as follows. Firstly, a conformance relation for TPAIO is introduced. Secondly, a polynomial method of test generation from a deterministic TPAIO with only lazy deadlines is defined. It consists of defining a polynomial algorithm that computes a partial reachability timed automaton by removing the stack constraints. This method is incomplete. The incompleteness is not a problem because software testing is an incomplete activity by nature. Thirdly, we define a method for generating test cases from a deterministic TPAIO with only outputs and delayable deadlines. It applies to the abstractions of timed recursive programs. It consists of generating test cases by computing an over-approximated tester. Finally, we propose a generalization of the test generation process from a non deterministic TPAIO with any deadlines. Its ability to detect non conform implementation is assessed by a mutation technique.

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.

Ce manuscrit a été rédigé en vue d'obtenir l'habilitation à diriger des recherches. J'y présente mon implication dans l'enseignement supérieur et la recherche au sein de l'Université d'Angers depuis mon recrutement en tant que maître de conférences, et plus précisément en tant qu'enseignant à l'ISTIA et en tant que chercheur au LISA. Au LISA, dirigé par Jean-Louis Ferrier au moment de mon recrutement, j'ai intégré l'équipe Modèles et Systèmes Dynamiques. Mon travail de recherche a profité des interactions avec les différents membres de cette équipe, et en particulier avec Jean-Louis Boimond (comme le laisseront apparaître les références dans la suite de ce manuscrit). Il concerne le comportement temporisé des systèmes à événements discrets en utilisant des modèles définis sur une structure algébrique de semi-anneau idempotent, encore appelée dioïde. Le document est structuré de la manière suivante. - Le premier chapitre présente mon curriculum vitae ainsi qu'un survol général de mes activités de recherche. - Le deuxième chapitre fait une synthèse plus détaillée de travaux motivés par deux préoccupations principales durant ces onze dernières années : élargir la classe des modèles relevant de la théorie des systèmes sur l'algèbre des dioïdes ; appliquer les résultats de la théorie des systèmes sur les dioïdes à l'analyse des systèmes de transport. En annexe, trois publications sont jointes pour que le lecteur puisse trouver plus de détails sur ces travaux. - Dans le troisième et dernier chapitre, je tire un bilan et envisage des perspectives à mes travaux.

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.