Cette thèse porte sur la synthèse de superviseurs pour des systèmes a événements discrets temps-réel (SEDTRs) modélisés par des automates temporises (ATs). Comme l'espace d'états d'un AT est en général infini, et que la théorie du contrôle supervise de RAMADGE et WONHAM, que nous avons adaptée, est opérationnelle pour des automates a états finis (AEFs), nous avons utilisé l'approche consistant à transformer les ATs modélisant le procédé et la spécification sous la forme d'AEFs. Nous avons donc tout d'abord étendu et amélioré une méthode de transformation des ATs en AEFs particuliers appelés automates Set-Exp (ASEs). Cette méthode de transformation, appelée SetExp, permet de réduire le problème d'explosion des états et est appropriée pour le contrôle supervise de SEDTRs. Nous avons ensuite amélioré et étendu une méthode de contrôle centralise fondée sur SetExp, c'est-à-dire que les ATs modélisant le procédé et la spécification sont d'abord transformes en ASEs et le problème est résolu en adaptant la théorie de RAMADGE et WONHAM aux ASEs. Pour la résolution du problème de contrôle centralise, nous avons identifié les conditions d'existence de solution et avons proposé une procédure algorithmique pour la synthèse du superviseur le moins restrictif. Suite à cela, nous avons développé une méthode de contrôle modulaire, fondée sur SetExp et la méthode de contrôle centralise. Pour le contrôle modulaire également, nous avons identifié les conditions d'existence de solution et propose une procédure de synthèse de superviseurs modulaires les moins restrictifs. D'autre part, nous avons étendu la méthode de contrôle centralise fondée sur SetExp au cas où le superviseur a une observation partielle des événements du procédé. Pour cette méthode de contrôle sous observation partielle des événements, nous avons identifié les conditions d'existence de solution et propose une procédure pour synthétiser un superviseur sous observation partielle. Enfin, nous avons réalisé un outil logiciel appelé SEAtool, qui implémente la transformation SetExp et les méthodes de contrôle centralise et modulaire. Nous avons étudié, à l'aide de SEAtool, l'application de nos méthodes de contrôles centralise et modulaire a des systèmes concrets simples.

De part et d’autre de la Terre, on observe de plus en plus de phénomènes naturels dévastateurs, parmi lesquels les inondations constituent l’une des catastrophes les plus fréquentes. Ces dernières décennies d’importantes inondations ont été induites par les crues de rivières. Ces crues, dues à des pluies excessives ou aux eaux de ruissellement, causent sans cesse des pertes de vies humaines et des dégâts matériels importants. Pour remédier à ces problèmes, les réseaux hydrographiques sont de plus en plus équipés de moyens de détection de crues. Un facteur essentiel à la gestion de tels phénomènes est la réactivité. En effet, les gestionnaires des réseaux hydrographiques, dans ce genre de situation, doivent prendre rapidement des décisions importantes dans un contexte incertain, car la plupart de ces crues sont le fruit de phénomènes climatiques brusques, dont l’ampleur est difficile à évaluer avec précision. Nous proposons, dans ce mémoire, une méthode de gestion des crues dans des réseaux hydrographiques équipés de zones inondables contrôlées par des portes gravitationnelles. Dans un premier temps, nous avons modélisé notre méthode de gestion à l’aide d’un réseau de transport statique. Dans un second temps, nous l’avons enrichi en utilisant les réseaux de transport à retards dans le but de prendre en compte les temps de déplacement de la ressource gérée. Afin de pallier le problème de la taille importante des réseaux de transport à retards, nous avons élaboré un mécanisme de substitution combinant un réseau de transport statique réduit et une matrice de temporisation. De plus, ce mécanisme autorise la prise en compte des temps de transfert variables dépendant des débits, sans modification ni du réseau de transport, ni de la structure de la matrice de temporisation. Ce mécanisme permet donc une gestion simplifiée des temps de transferts, variables ou non. Avec ce mécanisme, l’évaluation du flot maximal à coût minimum, nous a permis, suivant les stratégies de gestion considérées, de consigner l’ouverture des portes des zones inondables afin d’écrêter la crue mais aussi afin de restituer cette eau stockée au moment opportun. Finalement, afin d’évaluer les apports de cette gestion, la méthode a été appliquée sur un cas d’étude basée sur un tronçon de rivière équipé de trois zones inondables et modélisé à l’aide de simulateurs hydrauliques combinant les approches de modélisation 1D et 2D. Les résultats de simulation obtenus ont montré que l’approche proposée permettait de réduire de manière significative les inondations en aval des cours d’eau. / On either side of the Earth, we observe more and more devastating natural phenomena. Amon these phenomena, floods are one of the most frequent and devastating natural disasters. During these last decades extensive flooding were caused by the flood of rivers. These floods due to excessive rainfall or runoff induce invariably the loss of human lives and material damages. To overcome these problems, water systems are increasingly equipped with means for detecting floods. A key factor in the management of such phenomena is responsiveness. Indeed, managers of river systems, faced to this kind of situation should quickly take important decisions in an uncertain context, as most of these floods are induced by abrupt climate events, whose magnitude is difficult to assess accuracy. We propose in this dissertation, a method of flood management in river systems equipped with flood zones controlled by gravitational gates. At first, we modeled our management method using a static transportation network. In a second step, we enriched it by using transportation networks with delays in order to take into account the travel time of the managed resource. The main difficulty of transportation networks with delays is their oversize. To overcome this problem, we developed an alternative mechanism combining a static reduced transportation network with a temporization matrix. Furthermore, this mechanism allows the consideration of variable time transfer depending on flows, without modification either on the transportation network, or on the structure of the temporization matrix. This mechanism allows simplified management of the transfer times, variable or not. With this mechanism, the evaluation of the minimum cost maximum flow allowed us, according to the management strategies considered, to compute the gate opening for floodplains in order to mitigate the flood but also to restore the water stored at the relevant time. Finally, to evaluate the contributions of this management, the method was applied to a case study based on a section of river equipped with three flood control reservoirs areas modeled using hydraulic simulators combining 1D and 2D models. The simulation results showed that the proposed approach allowed reducing significantly the floods downstream watercourses.

De nos jours, les systèmes technologiques sont devenus très complexes (matériel informatique, logiciel, système de télécommunication, usine manufacturière, etc.), et cette complexité croît continuellement de sorte que les anciennes techniques intuitives utilisées pour leur conception, leur étude et leur réalisation deviennent inadaptées. À cause de cette complexité croissante, la probabilité pour qu'une erreur (ou panne) inattendue survienne est de plus en plus grande. Plus encore, quelques erreurs peuvent provoquer des accidents très graves causant des pertes économiques ou humaines. C'est dans ce cadre que les méthodes formelles ont été développées pour l'analyse, la conception et la réalisation des systèmes logiciels et électroniques quelque [i.e. quelle que] soit leur complexité. Ainsi, l'étude des systèmes à événements discrets (SED) a été introduite avec l'objectif de développer des méthodes formelles pour répondre à des besoins pressants, tels que le contrôle, le diagnostic, le pronostic, le test et la vérification des comportements discrets des systèmes technologiques. Cette thèse considère et généralise les études du contrôle et du diagnostic décentralisés des SED. Le principe commun du contrôle et du diagnostic décentralisés des SED est la prise de décision décentralisée, qui est basée sur l'utilisation d'une architecture décentralisée. Cette dernière est constituée de plusieurs décideurs locaux qui observent partiellement un SED et prennent des décisions locales qui sont ensuite fusionnées par un module de fusion D. Ce dernier, en se basant sur une fonction de fusion, calcule à partir des décisions locales une décision globale. Le système englobant les décideurs locaux et le module de fusion s'appelle un décideur décentralisé. L'ensemble de tous les décideurs décentralisés ayant D comme module de fusion est appelé D-architecture. La principale contribution de cette thèse est de proposer une nouvelle approche de prise de décision décentralisée, appelée multi-décision et qualifiée de multi-décisionnelle. Le principe de la multi-décision est basé sur l'utilisation de plusieurs (disons p) décideurs décentralisés (DD[indice supérieur j)[indice inférieur j=1,...,p] qui fonctionnent simultanément et en parallèle. Chaque DD[indice supérieur J] a une architecture décentralisée parmi celles qu'on trouve dans la littérature. C'est-à-dire que chaque DD[indice supérieur J] est constitué d'un ensemble de décideurs locaux ([Dec[indice supérieur J][indice inférieur i])[indice inférieur i=1,...,n] dont les décisions locales sont fusionnées par un module de fusion D[indice supérieur j] afin d'obtenir une décision globale. Dans l'architecture multi-décisionnelle, les décisions globales des p (DD[indice supérieur j])[indice inférieur j=1,...,p] sont fusionnées par un module D afin d'obtenir une décision effective qui respecte une propriété désirée Pr. L'intérêt de la multi-décision est que l'architecture ((DD[indice supérieur j])[indice inférieur j=1,..., p], D) constituée des différents (DD[indice supérieur j])[indice inférieur j =1,...,p] et de D généralise chacune des architectures DD[indice supérieur j]. C'est-à-dire que l'ensemble des SED auxquels on peut appliquer ((DD[indice supérieur j])[indice inférieur j=1,...,p], D) englobe les différents SED auxquels on peut appliquer les différents DD[indice supérieur j] séparément. Nous avons étudié l'approche multi-décisionnelle sur deux exemples de prise de décision : le contrôle supervisé et le diagnostic. On obtient alors le contrôle et le diagnostic multi-décisionnels. Dans les deux cas, l'approche multi-décisionnelle nécessite une décomposition de langages infinis (c.-à-d., contenant un nombre infini de séquences), qui est connue comme étant un problème difficile. Pour résoudre ce problème, on a proposé, dans le cas particulier des langages réguliers, une méthode qui transforme la décomposition d'un langage infini X en une décomposition d'un ensemble fini d'états marqués. Pour arriver à cela, on a dû s'imposer une restriction en ne considérant que les décompositions de X qui respectent une condition spécifique. Cette condition présente l'avantage de rendre les conditions d'existence de solutions vérifiables. Nous avons ainsi développé des algorithmes pour vérifier les conditions d'existence de solutions pour le contrôle et le diagnostic multi-décisionnels. Ces algorithmes ont le même ordre de complexité que les algorithmes qui vérifient les conditions d'existence de solutions pour le contrôle et le diagnostic décentralisés. Il est important de noter que les conditions d'existence obtenues pour une architecture multi-décisionnelle ((DD[indice supérieur j])[indice inférieur j=1,..., p], D) sont moins contraignantes que celles obtenues pour chacune des architectures DD[indice supérieur j].

La confiance de l'homme envers la machine est une caractéristique essentielle du contrôle supervisé. En effet, des contres performances du couple homme-machine provoquées par un mauvais niveau de confiance (insuffisant ou excessif) peuvent conduire à des dégâts matériels ou humains. Il est donc nécessaire d'évaluer la confiance de l'homme pour anticiper de telles situations et ainsi empêcher leur réalisation. C'est pourquoi, dans cette thèse, nous proposons un modèle d'évaluation de la confiance. Pour cela, nous avons défini deux modèles. Le premier est un modèle de dialogue basé sur la théorie du grounding et spécifique au contrôle supervisé. Le second est un modèle d'évaluation de la confiance qui décrit le lien entre la confiance de l'homme et l'observation de sa stratégie de dialogue à l'aide du premier modèle. Cet apport théorique est accompagné de deux expérimentations. Elles sont contextualisées dans le domaine du contrôle multi-drones et plus spécifiquement pour les opérations de surveillance et d'interception. La première expérience, à but exploratoire, met en évidence l'existence d'un lien entre confiance et dialogue. La seconde permet de tester la validation de notre modèle d'évaluation de la confiance. Cette thèse apporte donc les bases d'une approche objective de l'évaluation de la confiance à partir de l'observation du dialogue homme-machine.

A discrete event system is a system whose state space is given by a discrete set and whose state transition mechanism is event-driven i.e., its state evolution depends only on the occurrence of discrete events over the time. These systems are used in many fields of application (telecommunication networks, aeronautics, aerospace,...). The validity of these systems is then an important issue and to ensure it we can use supervisory control methods. These methods consist in imposing a given specification on a system by means of a controller which runs in parallel with the original system and which restricts its behavior. In this thesis, we develop supervisory control methods where the system can have an infinite state space and the controller has a partial observation of the system (this implies that the controller must define its control policy from an imperfect knowledge of the system). Unfortunately, this problem is generally undecidable. To overcome this negative result, we use abstract interpretation techniques which ensure the termination of our algorithms by overapproximating, however, some computations. The aim of this thesis is to provide the most complete contribution it is possible to bring to this topic. Hence, we consider more and more realistic problems. More precisely, we start our work by considering a centralized framework (i.e., the system is controlled by a single controller) and by synthesizing memoryless controllers (i.e., controllers that define their control policy from the current observation received from the system). Next, to obtain better solutions, we consider the synthesis of controllers that record a part or the whole of the execution of the system and use this information to define the control policy. Unfortunately, these methods cannot be used to control an interesting class of systems: the distributed systems. We have then defined methods that allow to control distributed systems with synchronous communications (decentralized and modular methods) and with asynchronous communications (distributed method). Moreover, we have implemented some of our algorithms to experimentally evaluate the quality of the synthesized controllers. / Un système à événements discrets est un système dont l'espace d'états est un ensemble discret et dont l'évolution de l'état courant dépend de l'occurrence d'événements discrets à travers le temps. Ces systèmes sont présents dans de nombreux domaines critiques tels les réseaux de communications, l'aéronautique, l'aérospatiale... La validité de ces systèmes est dès lors une question importante et une manière de l'assurer est d'utiliser des méthodes de contrôle supervisé. Ces méthodes associent au système un dispositif, appelé contrôleur, qui s'exécute en parrallèle et qui restreint le comportement du système de manière à empêcher qu'un comportement erroné ne se produise. Dans cette thèse, on s'intéresse au développement de méthodes de contrôle supervisé où le système peut avoir un espace d'états infini et où les contrôleurs ne sont pas toujours capables d'observer parfaitement le système; ce qui implique qu'ils doivent définir leur politique de contrôle à partir d'une connaissance imparfaite du système. Malheureusement, ce problème est généralement indécidable. Pour surmonter cette difficulté, nous utilisons alors des techniques d'interprétation abstraite qui assurent la terminaison de nos algorithmes au prix de certaines sur-approximations dans les calculs. Le but de notre thèse est de fournir la contribution la plus complète possible dans ce domaine et nous considèrons pour cela des problèmes de plus en plus réalistes. Plus précisement, nous avons commencé notre travail en définissant une méthode centralisée où le système est contrôlé par un seul contrôleur qui définit sa politique de contrôle à partir de la dernière information reçue du système. Ensuite, pour obtenir de meilleures solutions, nous avons défini des contrôleurs qui retiennent une partie ou la totalité de l'exécution du système et qui définissent leur politique de contrôle à partir de cette information. Malheureusement, ces méthodes ne peuvent pas être utilisées pour contrôler une classe intéressante de systèmes: les sytèmes distribués. Nous avons alors défini des méthodes permettant de contrôler des systèmes distribués dont les communications sont synchrones (méthodes décentralisées et modulaires) et asynchrones (méthodes distribuées). De plus, nous avons implémenté certains de nos algorithmes pour évaluer expérimentalement la qualité des contrôleurs qu'ils synthétisent.

Cette thèse contribue à l’étude de la fiabilité et de la sécurité-innocuité des systèmes informatisés, modélisés par des systèmes à événements discrets. Les principales contributions concernent la théorie des Systèmes de Contrôle (notés C Systems) et l’approche par Monitoring des modèles.Dans la première partie de la thèse, nous étudions la théorie des Systèmes de Contrôle qui combine et étend de façon significative, les systèmes de réécriture de la théorie des langages et le contrôle supervisé. Un système de contrôle est une structure générique qui contient deux composants : le composant contrôlé et le composant contrôlant qui restreint le comportement du composant contrôlé. Les deux composants sont exprimés en utilisant le même formalisme comme des automates ou des grammaires. Nous considérons différentes classes de systèmes de contrôle basés sur différents formalismes comme, par exemple, les automates, les grammaires, ainsi que leurs versions infinies et concurrentes. Ensuite, une application de cette théorie est présentée. Les systèmes de contrôle basés sur les automates de Büchi sont utilisés pour vérifier par model-checking, des propriétés définissant la correction sur des traces d’exécution spécifiées par une assertion de type nevertrace.Dans la seconde partie de la thèse, nous investiguons l’approche de monitoring des modèles dont la théorie des systèmes de contrôle constitue les fondations formelles. Le principe pivot de cette approche est la «spécification de propriétés comme contrôleur». En d’autres termes, pour un système, les exigences fonctionnelles, d’une part, et des propriétés, d’autre part, sont modélisées et implantées séparément, les propriétés spécifiées contrôlant le comportement issu des exigences fonctionnelles. De cette approche découle ainsi deux techniques alternatives, respectivement nommées monitoring de modèle et génération de modèle. Cette approche peut être utilisée de diverses manières pour améliorer la fiabilité et la sécurité-innocuité de divers types de systèmes. Nous présentons quelques applications qui montrent l’intérêt pratique de cette contribution théorique. Tout d’abord, cette approche aide à prendre en compte les évolutions des spécifications des propriétés. En second lieu, elle fournit une base théorique à la sécurité fonctionnelle, popularisée par la norme IEC 61508. En troisième lieu, l’approche peut être utilisée pour formaliser et vérifier l’application de guides de bonnes pratiques ou des règles de modélisation appliquées par exemple pour des modèles UML.Ces résultats constituent les bases pour des études futures de dispositifs plus perfectionnés, et fournissent une nouvelle voie pour s’assurer de la fiabilité et de la sécurité-innocuité des systèmes / This thesis contributes to the study of reliability and safety of computer and software systems which are modeled as discrete event systems. The major contributions include the theory of Control Systems (C Systems) and the model monitoring approach.In the first part of the thesis, we study the theory of control systems which combines and significantly extends regulated rewriting in formal languages theory and supervisory control. The control system is a generic framework, and contains two components: the controlled component and the controlling component that restricts the behavior of the controlled component. The two components are expressed using the same formalism, e.g., automata or grammars. We consider various classes of control systems based on different formalisms, for example, automaton control systems, grammar control systems, and their infinite versions and concurrent variants. After that, an application of the theory is presented. The Büchi automata based control system is used to model and check correctness properties on execution traces specified by nevertrace claims.In the second part of the thesis, we investigate the model monitoring approach whose theoretical foundation is the theory of control systems. The key principle of the approach is “property specifications as controllers”. In other words, the functional requirements and property specification of a system are separately modeled and implemented, and the latter one controls the behavior of the former one. The model monitoring approach contains two alternative techniques, namely model monitoring and model generating. The approach can be applied in several ways to improve reliability and safety of various classes of systems. We present some typical applications to show its strong power. First, the approach provides better support for the change and evolution of property specifications. Second, it provides the theoretical foundation of safety-related systems in the standard IEC 61508 for ensuring the functional validity. Third, it is used to formalize and check guidelines and consistency rules of UML.These results lay out the foundations for further study of more advanced control mechanisms, and provide a new way for ensuring reliability and safety

A discrete event system is a system whose state space is given by a discrete set and whose state transition mechanism is event-driven i.e. its state evolution depends only on the occurrence of discrete events over the time. These systems are used in many fields of application (telecommunication networks, aeronautics, aerospace,). The validity of these systems is then an important issue and to ensure it we can use supervisory control methods. These methods consist in imposing a given specification on a system by means of a controller which runs in parallel with the original system and which restricts its behavior. In this thesis, we develop supervisory control methods where the system can have an infinite state space and the controller has a partial observation of the system (this implies that the controller must define its control policy from an imperfect knowledge of the system). Unfortunately, this problem is generally undecidable. To overcome this negative result, we use abstract interpretation techniques which ensure the termination of our algorithms by overapproximating, however, some computations. The aim of this thesis is to provide the most complete contribution it is possible to bring to this topic. Hence, we consider more and more realistic problems. More precisely, we start our work by considering a centralized framework (i.e. the system is controlled by a single controller) and by synthesizing memoryless controllers (i.e. controllers that define their control policy from the current observation received from the system). Next, to obtain better solutions, we consider the synthesis of controllers that record a part or the whole of the execution of the system and use this information to define the control policy. Unfortunately, these methods cannot be used to control an interesting class of systems: the distributed systems. We have then defined methods that allow to control distributed systems with synchronous communications (decentralized and modular methods) and with asynchronous communications (distributed method). Moreover, we have implemented some of our algorithms to experimentally evaluate the quality of the synthesized controllers. / <p><p>Un système à événements discrets est un système dont l'espace d'états est un ensemble discret et dont l'évolution de l'état courant dépend de l'occurrence d'événements discrets à travers le temps. Ces systèmes sont présents dans de nombreux domaines critiques tels les réseaux de communications, l'aéronautique, l'aérospatiale. La validité de ces systèmes est dès lors une question importante et une manière de l'assurer est d'utiliser des méthodes de contrôle supervisé. Ces méthodes associent au système un dispositif, appelé contrôleur, qui s'exécute en parrallèle et qui restreint le comportement du système de manière à empêcher qu'un comportement erroné ne se produise. Dans cette thèse, on s'intéresse au développement de méthodes de contrôle supervisé où le système peut avoir un espace d'états infini et où les contrôleurs ne sont pas toujours capables d'observer parfaitement le système; ce qui implique qu'ils doivent définir leur politique de contrôle à partir d'une connaissance imparfaite du système. Malheureusement, ce problème est généralement indécidable. Pour surmonter cette difficulté, nous utilisons alors des techniques d'interprétation abstraite qui assurent la terminaison de nos algorithmes au prix de certaines sur-approximations dans les calculs. Le but de notre thèse est de fournir la contribution la plus complète possible dans ce domaine et nous considèrons pour cela des problèmes de plus en plus réalistes. Plus précisement, nous avons commencé notre travail en définissant une méthode centralisée où le système est contrôlé par un seul contrôleur qui définit sa politique de contrôle à partir de la dernière information reçue du système. Ensuite, pour obtenir de meilleures solutions, nous avons défini des contrôleurs qui retiennent une partie ou la totalité de l'exécution du système et qui définissent leur politique de contrôle à partir de cette information. Malheureusement, ces méthodes ne peuvent pas être utilisées pour contrôler une classe intéressante de systèmes: les sytèmes distribués. Nous avons alors défini des méthodes permettant de contrôler des systèmes distribués dont les communications sont synchrones (méthodes décentralisées et modulaires) et asynchrones (méthodes distribuées). De plus, nous avons implémenté certains de nos algorithmes pour évaluer expérimentalement la qualité des contrôleurs qu'ils synthétisent. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished