Notre travail de recherche concerne l'étude de la commande à base de modèles pour une sous-classe de systèmes dynamiques hybrides (SDH). L'outil de modélisation choisi est l'automate hybride rectangulaire (AHR) pour sa puissance d'analyse. Nous proposons ainsi une méthode pour la synthèse de la commande des SDH modélisés par des AHR. Cette méthode repose sur l'application d'une procédure amont/aval de commande hors-ligne qui détermine d'une façon maximale permissive les nouvelles gardes de transition de l'automate respectant des spécifications de commande imposées par l'utilisateur. Tous les calculs réalisés reposent sur la détermination de la durée de séjour, valeur contrainte par l'espace atteignable du sommet correspondant. La garde portant à la fois sur l'état continu et sur l'événement discret, la commande se fait par ce dernier car il s'agit du seul élément contrôlable. Nous nous intéressons alors à la construction du contrôleur temporisé autorisant l'occurrence des événements contrôlables du système dans un intervalle d'horloge défini au sens de la maximale permissivité.

Notre travail de recherche concerne l’étude de la commande à base de modèles pour une sous-classe de systèmes dynamiques hybrides (SDH). L’outil de modélisation choisi est l’automate hybride rectangulaire (AHR) pour sa puissance d’analyse. Nous proposons ainsi une méthode pour la synthèse de la commande des SDH modélisés par des AHR. Cette méthode repose sur l’application d’une procédure amont/aval de commande hors-ligne qui détermine d’une façon maximale permissive les nouvelles gardes de transition de l’automate respectant des spécifications de commande imposées par l’utilisateur. Tous les calculs réalisés reposent sur la détermination de la durée de séjour, valeur contrainte par l’espace atteignable du sommet correspondant. La garde portant à la fois sur l’état continu et sur l’événement discret, la commande se fait par ce dernier car il s’agit du seul élément contrôlable. Nous nous intéressons alors à la construction du contrôleur temporisé autorisant l’occurrence des événements contrôlables du système dans un intervalle d’horloge défini au sens de la maximale permissivité. / In this thesis, we study the control of a class of hybrid dynamic systems (HDS). The chosen modeling tool is the rectangular hybrid automaton (RHA) for his analysis power. We propose a method for the control synthesis of HDS modeled with RHA. This method consists on the application of a downstream/upstream offline control procedure that determines in a maximal permissive way the new automaton transition guards respecting the desired control specifications. All computations are based on the determination of the duration of stay, a value constrained by the reachable space of the corresponding location. Since the guard refers to both continuous state and discrete event, the control is made by the latter because it is the controllable element. Then we are interested in the construction of the timed controller authorizing the system controllable event occurrence in a clock interval defined in a maximal permissive way.

Abstract: Fault tolerance is an essential property to be satis ed in the composition of services, but reaching a high level of fault tolerance remains a challenge. In the area of ubiquitous computing, the composition of services is inevitable when a request cannot be carried out by a single service, but by a combination of several services. This thesis studies fault tolerance in the context of a general behavior composition framework. This approach raises, rst, the problem of the synthesis of controllers (or compositions) in order to coordinate a set of available services to achieve a new service, the target service and, second, the exploitation of all compositions to make the new service fault tolerant. Although a solution has been proposed by the authors of the behavior composition framework, it is incomplete and has not been evaluated experimentally or in situ. This thesis brings two contributions to this problem. On one hand, it considers the case in which the service selected by the controller is temporarily or permanently unavailable by exploiting recovery techniques to identify a consistent state of the system from which it may progress using other services or leave it in a coherent state when none of the available services no longer allows progression. On the other hand, it evaluates several recovery solutions, each useful in services malfunction situations, using a case study implemented with the aid of Akka, a tool that facilitates the development of reactive, concurrent and distributed systems. / La tolérance aux fautes est une propriété indispensable à satisfaire dans la composition de services, mais atteindre un haut de niveau de tolérance aux fautes représente un défi majeur. Dans l'ère de l'informatique ubiquitaire, la composition de services est inévitable lorsqu'une requête ne peut être réalisée par un seul service, mais par la combinaison de plusieurs services. Ce mémoire étudie la tolérance aux fautes dans le contexte d'un cadre général de composition de comportements (behavior composition framework en anglais). Cette approche soulève, tout d'abord, le problème de la synthèse de contrôleurs (ou compositions) de façon à coordonner un ensemble de services disponibles afin de réaliser un nouveau service, le service cible et, ensuite, celui de l'exploitation de l'ensemble des compositions afin de rendre le nouveau service tolérant aux fautes. Bien qu'une solution ait été proposée par les auteurs de ce cadre de composition, elle est incomplète et elle n'a pas été évaluée expérimentalement ou in situ. Ce mémoire apporte deux contributions à ce problème. D'une part, il considère le cas dans lequel le service visé par le contrôleur est temporairement ou définitivement non disponible en exploitant des techniques de reprise afin d'identifier un état cohérent du système à partir duquel il peut progresser en utilisant d'autres services ou de le laisser dans un état cohérent lorsqu'aucun service, parmi ceux disponibles, ne permet plus de progression. D'autre part, il évalue plusieurs solutions de reprise, chacune utile dans des situations particulières de pannes, à l'aide d'une étude de cas implémentée en Akka, un outil qui permet aisément de mettre en oeuvre des systèmes réactifs, concurrents et répartis.

Abstract: Fault tolerance is an essential property to be satis ed in the composition of services, but reaching a high level of fault tolerance remains a challenge. In the area of ubiquitous computing, the composition of services is inevitable when a request cannot be carried out by a single service, but by a combination of several services. This thesis studies fault tolerance in the context of a general behavior composition framework. This approach raises, rst, the problem of the synthesis of controllers (or compositions) in order to coordinate a set of available services to achieve a new service, the target service and, second, the exploitation of all compositions to make the new service fault tolerant. Although a solution has been proposed by the authors of the behavior composition framework, it is incomplete and has not been evaluated experimentally or in situ. This thesis brings two contributions to this problem. On one hand, it considers the case in which the service selected by the controller is temporarily or permanently unavailable by exploiting recovery techniques to identify a consistent state of the system from which it may progress using other services or leave it in a coherent state when none of the available services no longer allows progression. On the other hand, it evaluates several recovery solutions, each useful in services malfunction situations, using a case study implemented with the aid of Akka, a tool that facilitates the development of reactive, concurrent and distributed systems. / La tolérance aux fautes est une propriété indispensable à satisfaire dans la composition de services, mais atteindre un haut de niveau de tolérance aux fautes représente un défi majeur. Dans l'ère de l'informatique ubiquitaire, la composition de services est inévitable lorsqu'une requête ne peut être réalisée par un seul service, mais par la combinaison de plusieurs services. Ce mémoire étudie la tolérance aux fautes dans le contexte d'un cadre général de composition de comportements (behavior composition framework en anglais). Cette approche soulève, tout d'abord, le problème de la synthèse de contrôleurs (ou compositions) de façon à coordonner un ensemble de services disponibles afin de réaliser un nouveau service, le service cible et, ensuite, celui de l'exploitation de l'ensemble des compositions afin de rendre le nouveau service tolérant aux fautes. Bien qu'une solution ait été proposée par les auteurs de ce cadre de composition, elle est incomplète et elle n'a pas été évaluée expérimentalement ou in situ. Ce mémoire apporte deux contributions à ce problème. D'une part, il considère le cas dans lequel le service visé par le contrôleur est temporairement ou définitivement non disponible en exploitant des techniques de reprise afin d'identifier un état cohérent du système à partir duquel il peut progresser en utilisant d'autres services ou de le laisser dans un état cohérent lorsqu'aucun service, parmi ceux disponibles, ne permet plus de progression. D'autre part, il évalue plusieurs solutions de reprise, chacune utile dans des situations particulières de pannes, à l'aide d'une étude de cas implémentée en Akka, un outil qui permet aisément de mettre en oeuvre des systèmes réactifs, concurrents et répartis.

Les systèmes hybrides sont des systèmes qui combinent des dynamiques discrètes et continues. Cette thèse propose des techniques algorithmiques de vérification et de synthèse pour ces systèmes Le manque de méthodes pour calculer les ensembles atteignables des dynamiques continues est l'obstacle principal vers une méthodologie algorithmique de vérification. Nous développons deux techniques d'atteignabilité approximatives pour les systèmes continus basées sur une méthode efficace pour représenter des ensembles et une combinaison des techniques de la simulation, de la géométrie algorithmique, de l'optimisation, et de la commande optimale. La première technique d'atteignabilité est spécialisée pour les systèmes linéaires et étendue aux systèmes avec entrée incertaine, et la seconde peut être appliquée aux systèmes non-linéaires. En appliquant ces techniques nous développons un algorithme de vérification des propriétés de sûreté pour une large classe des systèmes hybrides avec des dynamiques continues arbitraires et des dynamiques discrètes assez générales. Nous étudions ensuite le problème de la synthèse de contrôleurs de sûreté pour les systèmes hybrides. Nous présentons un algorithme de synthèse des contrôleurs par commutation basé sur le calcul de l'ensemble d'invariance maximal et les techniques d'analyse d'atteignabilité. Nous avons implanté les algorithmes développés dans un outil appelé "d/dt", qui permet la vérification et la synthèse automatique pour les systèmes hybrides avec des inclusions différentielles linéaires. En dehors de nombreux exemples académiques, nous avons appliqué avec succès l'outil pour analyser quelques systèmes pratiques.

Le contrôle de systèmes industriels à cause de l’automatisation et la réduction de nombre des opérateurs devient un enjeu crucial. Les systèmes de production automatisés (AMS) sont d’autant plus touchés car une défaillance du programme de contrôle peut réduire considérablement la productivité voire entraîner l’arrêt du système de production. Pour certains de ces systèmes où le partage des ressources est pondérant, la notion de blocage partiel ou global est fréquente et la validation avant implantation est préférable pour réduire les risques.En raison de la capacité des réseaux de Petri à décrire aisément l’exécution concurrente des processus et le partage des ressources, de nombreuses méthodes de vérification d’absence de blocage et de synthèse de contrôleurs basées sur la théorie structurelle ou le graphe d’accessibilité des réseaux de Petri ont été proposées au cours des deux dernières décennies.Traditionnellement, une méthode de prévention de blocage est évaluée selon trois critères de performance: la complexité structurelle, la permissivité comportementale, et la complexité de calcul. Les méthodes fondées sur l’espace d’état aboutissent généralement à un contrôle maximal permissif mais souffrent de l'explosion combinatoire de l'espace d'états. En revanche, les méthodes de synthèse de contrôleurs fondées sur l’analyse structurelle évitent le problème de l’explosion de l’espace d’état mais aboutissent à des superviseurs pouvant restreindre considérablement les comportements admissibles du système. De plus si la théorie structurelle de contrôle de siphons pour la synthèse des superviseurs est mature dans le cas des réseaux de Petri ordinaires, elle est en développement pour les réseaux de Petri généralises. Par ailleurs, la plupart des travaux existants partent du principe que les ressources sont constamment disponibles. Or l’indisponibilité de ressources est en réalité un phénomène ordinaire. Il serait donc judicieux de développer une politique de vérification de blocage qui soit efficace tout en considérant des ressources non fiables.Cette thèse vise principalement à faire face aux limitations mentionnées ci-dessus. Nos principales contributions à la fois théoriques et algorithmiques sont les suivantes.Premièrement, après avoir revisité les conditions de contrôlabilité des siphons (cs–propriété) et précisé les limitations de la max cs- propriété et max’ cs- propriété, nous définissons la max’’ cs-propriété et nous démontrons que cette nouvelle propriété est une condition non seulement suffisante mais aussi nécessaire pour la vivacité de la classe des GS3PR (Generalized Systems of SimpleSequential Processes with Resources).Par la suite nous montrons comment le problème de la vérification de cette propriété et donc la vivacité des GS3PR peut se ramener à la résolution d’un programme linéaire en nombre entiers.Dans une seconde partie, nous proposons une classe de réseaux de Petri appelée M-Nets dotée d’une forte capacité de modélisation des systèmes de production automatisés. En combinant la théorie du contrôle siphon avec la théorie des régions, nous développons une méthode de prévention de blocage ayant un bon compromis entre l'optimalité du comportement et la complexité de calcul. De plus, nous proposons une méthode de synthèse d'un contrôleur maximal permissif pour une sous-classe de réseaux notée b-nets.Enfin, nous proposons dans cette thèse une méthode de conception d’un superviseur de systèmes de production automatisés où les ressources ne sont pas toutes fiables et particulièrement efficace pour la classe des S3PR (Systems of Simple Sequential Processes with Resources). / Because of automation and reduction of the number of operators, the control of industrial systems is becoming a critical issue. For automated manufacturing systems (AMS) where resource sharing is preponderant, the notion of partial or total blocking is frequent and validation before implementation is preferable to reduce the risks.Due to the easy and concise description of the concurrent execution of processes and the resource sharing by Petri nets, many methods to verify deadlock-freeness and to synthesize controllers using structural theory or reachability graph have been proposed over the past two decades.Traditionally, a deadlock control policy can be evaluated by three performance criteria : structural complexity, behavioral permissiveness, and computational complexity. Generally, deadlock control policies based on the state space analysis can approach the maximal permissive behavior, but suffer from the state explosionproblem. On the contrary deadlock control policies based on the structural analysis of Petri nets avoid in general the state explosion problem successfully, but cannot lead to the maximally or near maximally permissive controller. Morover, the current Deadlock control theory based on siphons is fairly mature for ordinary Petri nets,while for generalized Petri nets, it is presently at an early stage.On the other hand, most deadlock control policies based on Petri nets for AMS proceed on the premise that the resources in a system under consideration are reliable. Actually, resource failures are inevitable and common in most AMS, which may also cause processes to halt. Therefore, it is judicious to develop an effective and robust deadlock control policy considering unreliable resources.This thesis aims to cope with the limitations mentioned above. Our main theoretical and algorithmic contributions are the following. Firstly, after revisiting the controllability conditions of siphons and limitations of max and max' controlled-siphon properties, we define the max'' cs property and we prove that this new cs-property is not only sufficient but also a necessary liveness condition forgeneralized systems of simple sequential processes with resources (GS3PR). Moreover, we show how the checking of this property and hence liveness of GS3PR nets can be translaled into resolution of an integer programming (IP) model.Secondly, we propose a class of manufacturing-oriented Petri nets, M-nets for short, with strong modeling capability. Combining siphon control and the theory of regions, we develop a deadlock prevention method that makes a good trade-off between behavioral optimality and computational tractability Moreover, this thesis proposes a maximally permissive control policy for a subclass of Petri nets (calledBéta-nets) based on the token distribution pattern of unmarked siphons.Finally, we propose a designs method for robust liveness-enforcingsupervisors for AMS with unreliable resources appropriate in particular for systems of simple sequential processes with resources(S3PR)

Ce manuscrit présente des résultats de recherche concernant une certaine classe de systèmes hybrides. Les systèmes hybrides peuvent être utilisés pour la modélisation de systèmes physiques complexes et hétérogènes dont l'évolution dans le temps présente des phénomènes discrets, tels que les commutations des convertisseurs ou les impacts des systèmes mécaniques. De la même manière, la théorie hybride peut être utilisée pour concevoir des contrôleurs hybrides, en général plus performants par rapport aux contrôleurs à temps continu. Dans ce cadre, les résultats de ce manuscrit peuvent être divisés en trois parties. D'abord des résultats de stabilité par rapport à un indice de performance de type Hinfini sont présentés pour une classe plutôt large de systèmes hybrides. Ensuite, nous introduisons de nouvelles architectures de contrôleurs hybrides pour les systèmes à temps continu, caractérisées par le fait que leur état peut être réinitialisé en fonction de la trajectoire. Enfin, nous présentons une technique de synthèse convexe pour la conception d'un contrôleur hybride multi-objectif. La comparaison avec les résultats classique met en évidence les avantages en termes de performance par rapport aux contrôleurs à temps continu classiques, tout en préservant la propriété de robustesse et la simplicité de conception. Bien que la théorie hybride soit en plein développement, ces travaux généralisent certains résultats existants, en améliorant la simplicité d'implémentation des solutions grâce à l'utilisation de la programmation semi-définie. En plus les architectures de contrôleurs hybrides présentées ont l'avantage de simplifier la généralisation de quelques résultats classiques concernant la synthèse optimale par rapport à des indices de performance communs.

La méthode des invariants est une des plus utilisées méthodes de synthèse pour les SED modélisés par des réseaux de Petri (RdP). Cependant, elle ne garantit pas en général une solution optimale dans la présence de l'incontrôlabilité. Dans ce travail nous proposons une solution à ce problème pour les RdP généralisés. Premièrement, nous proposons une solution d'identification des contraintes admissibles pour les RdP saufs non-conservatifs. La méthode repose sur une définition des contraintes contenant des marquages complémentés. Ceux-ci sont après éliminés en exploitant les composants conservatifs des RdP. Deuxièmement, nous avançons une technique de détermination des contraintes admissibles pour les RdP généralisés. La méthode est basée sur une vision spatiale de l'espace d'états du modèle. Les contraintes sont dérivées de l'équation d'hyperplan affin qui sépare les régions interdite- et autorisée- de cet espace. Nous proposons un algorithme pour le calcul du contrôleur optimal minimal.

Le contrôle de systèmes industriels à cause de l’automatisation et la réduction de nombre des opérateurs devient un enjeu crucial. Les systèmes de production automatisés (AMS) sont d’autant plus touchés car une défaillance du programme de contrôle peut réduire considérablement la productivité voire entraîner l’arrêt du système de production. Pour certains de ces systèmes où le partage des ressources est pondérant, la notion de blocage partiel ou global est fréquente et la validation avant implantation est préférable pour réduire les risques.En raison de la capacité des réseaux de Petri à décrire aisément l’exécution concurrente des processus et le partage des ressources, de nombreuses méthodes de vérification d’absence de blocage et de synthèse de contrôleurs basées sur la théorie structurelle ou le graphe d’accessibilité des réseaux de Petri ont été proposées au cours des deux dernières décennies.Traditionnellement, une méthode de prévention de blocage est évaluée selon trois critères de performance: la complexité structurelle, la permissivité comportementale, et la complexité de calcul. Les méthodes fondées sur l’espace d’état aboutissent généralement à un contrôle maximal permissif mais souffrent de l'explosion combinatoire de l'espace d'états. En revanche, les méthodes de synthèse de contrôleurs fondées sur l’analyse structurelle évitent le problème de l’explosion de l’espace d’état mais aboutissent à des superviseurs pouvant restreindre considérablement les comportements admissibles du système. De plus si la théorie structurelle de contrôle de siphons pour la synthèse des superviseurs est mature dans le cas des réseaux de Petri ordinaires, elle est en développement pour les réseaux de Petri généralises. Par ailleurs, la plupart des travaux existants partent du principe que les ressources sont constamment disponibles. Or l’indisponibilité de ressources est en réalité un phénomène ordinaire. Il serait donc judicieux de développer une politique de vérification de blocage qui soit efficace tout en considérant des ressources non fiables.Cette thèse vise principalement à faire face aux limitations mentionnées ci-dessus. Nos principales contributions à la fois théoriques et algorithmiques sont les suivantes.Premièrement, après avoir revisité les conditions de contrôlabilité des siphons (cs–propriété) et précisé les limitations de la max cs- propriété et max’ cs- propriété, nous définissons la max’’ cs-propriété et nous démontrons que cette nouvelle propriété est une condition non seulement suffisante mais aussi nécessaire pour la vivacité de la classe des GS3PR (Generalized Systems of SimpleSequential Processes with Resources).Par la suite nous montrons comment le problème de la vérification de cette propriété et donc la vivacité des GS3PR peut se ramener à la résolution d’un programme linéaire en nombre entiers.Dans une seconde partie, nous proposons une classe de réseaux de Petri appelée M-Nets dotée d’une forte capacité de modélisation des systèmes de production automatisés. En combinant la théorie du contrôle siphon avec la théorie des régions, nous développons une méthode de prévention de blocage ayant un bon compromis entre l'optimalité du comportement et la complexité de calcul. De plus, nous proposons une méthode de synthèse d'un contrôleur maximal permissif pour une sous-classe de réseaux notée b-nets.Enfin, nous proposons dans cette thèse une méthode de conception d’un superviseur de systèmes de production automatisés où les ressources ne sont pas toutes fiables et particulièrement efficace pour la classe des S3PR (Systems of Simple Sequential Processes with Resources). / Because of automation and reduction of the number of operators, the control of industrial systems is becoming a critical issue. For automated manufacturing systems (AMS) where resource sharing is preponderant, the notion of partial or total blocking is frequent and validation before implementation is preferable to reduce the risks.Due to the easy and concise description of the concurrent execution of processes and the resource sharing by Petri nets, many methods to verify deadlock-freeness and to synthesize controllers using structural theory or reachability graph have been proposed over the past two decades.Traditionally, a deadlock control policy can be evaluated by three performance criteria : structural complexity, behavioral permissiveness, and computational complexity. Generally, deadlock control policies based on the state space analysis can approach the maximal permissive behavior, but suffer from the state explosionproblem. On the contrary deadlock control policies based on the structural analysis of Petri nets avoid in general the state explosion problem successfully, but cannot lead to the maximally or near maximally permissive controller. Morover, the current Deadlock control theory based on siphons is fairly mature for ordinary Petri nets,while for generalized Petri nets, it is presently at an early stage.On the other hand, most deadlock control policies based on Petri nets for AMS proceed on the premise that the resources in a system under consideration are reliable. Actually, resource failures are inevitable and common in most AMS, which may also cause processes to halt. Therefore, it is judicious to develop an effective and robust deadlock control policy considering unreliable resources.This thesis aims to cope with the limitations mentioned above. Our main theoretical and algorithmic contributions are the following. Firstly, after revisiting the controllability conditions of siphons and limitations of max and max' controlled-siphon properties, we define the max'' cs property and we prove that this new cs-property is not only sufficient but also a necessary liveness condition forgeneralized systems of simple sequential processes with resources (GS3PR). Moreover, we show how the checking of this property and hence liveness of GS3PR nets can be translaled into resolution of an integer programming (IP) model.Secondly, we propose a class of manufacturing-oriented Petri nets, M-nets for short, with strong modeling capability. Combining siphon control and the theory of regions, we develop a deadlock prevention method that makes a good trade-off between behavioral optimality and computational tractability Moreover, this thesis proposes a maximally permissive control policy for a subclass of Petri nets (calledBéta-nets) based on the token distribution pattern of unmarked siphons.Finally, we propose a designs method for robust liveness-enforcingsupervisors for AMS with unreliable resources appropriate in particular for systems of simple sequential processes with resources(S3PR)

Dans cette thèse, nous nous intéressons à la spécification et à la synthèse de contrôleurs des systèmes temps-réels. Les modèles pour ces systèmes sont des Event-recording Automata. Nous supposons que les contrôleurs observent tous les évènements se produisant dans le système et qu'ils peuvent interdirent uniquement des évènements contrôlables. Tous les évènements ne sont pas nécessairement contrôlables. Une première étude est faite sur la logique Event-recording Logic (ERL). Nous proposons des nouveaux algorithmes pour les problèmes de vérification et de satisfaisabilité. Ces algorithmes présentent les similitudes entre les problèmes de décision cités ci-dessus et les problèmes de décision similaires étudiés dans le cadre du $\mu$-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la litérature. Les similitudes relevées nous permettent de prouver l'équivalence entre les formules de ERL et les formules de ERL en forme normale disjonctive. La logique ERL n'étant pas suffisamment expressive pour décrire certaines propriétés des systèmes, en particulier des propriétés des contrôleurs, nous introduisons une nouvelle logique WTmu. La logique WTmu est une extension temps-réel faible du $\mu$-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WTmu. Nous identifions un fragment de WTmu appelé WTmu pour le contrôle (C-WTmu). Nous proposons un algorithme qui permet de vérifier si une formule de C-WTmu possède un modèle. Cet algorithme n'a pas besoin de connaître les ressources (horloges et constante maximale comparée avec les horloges) des modèles. En utilisant C-WTmu comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le $\Delta$-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contrôleurs.