Les systèmes actuels deviennent chaque jour de plus en plus complexe; à la distribution s’ajoutent les contraintes temps réel. Les méthodes classiques en charge de garantir la sûreté de fonctionnement, comme le test, l’injection de fautes ou les méthodes formelles ne sont plus suffisantes à elles seules. Afin de pouvoir traiter les éventuelles erreurs lors de leur apparition dans un système distribué donné, nous désirons mettre en place un programme, surveillant ce système, capable de lancer une alerte lorsque ce dernier s’éloigne de ses spécifications ; un tel programme est appelé superviseur (ou moniteur). Le fonctionnement d’un superviseur consiste simplement à interpréter un ensemble d’informations provenant du système sous forme de message, que l’on qualifiera d’évènement, et d’en déduire un diagnostic. L’objectif de cette thèse est de mettre un place un superviseur distribué permettant de vérifier en temps réel des propriétés temporelles. En particulier nous souhaitons que notre moniteur soit capable de vérifier un maximum de propriétés avec un minimum d’information. Ainsi notre outil est spécialement conçu pour fonctionner parfaitement même si l’observation est imparfaite, c’est-à-dire, même si certains évènements arrivent en retard ou s’ils ne sont jamais reçus. Nous avons de plus cherché à atteindre cet objectif de manière distribuée pour des raisons évidentes de performance et de tolérance aux fautes. Nous avons ainsi proposé un protocole distribuable fondé sur l’exécution répartie d’un réseau de Petri temporisé. Pour vérifier la faisabilité et l’efficacité de notre approche, nous avons mis en place une implémentation appelée Minotor qui s’est révélée avoir de très bonnes performances. Enfin, pour montrer l’expressivité du formalisme utilisé pour exprimer les spécifications que l’on désire vérifier, nous avons détaillé un ensemble de propriétés sous forme de réseaux de Petri à double sémantique introduite dans cette thèse (l’ensemble des transitions étant partitionné en deux catégories de transitions, chacune de ces parties ayant sa propre sémantique). / Current systems are becoming every day more and more complex, being both distributed and real-timed. Conventional methods responsible for guaranteeing dependability, such as testing, fault injection or formal methods are no longer sufficient. In order to process any errors when they appear in a given distributed system, we want to implement a software monitoring it and capable of launching an alert when the system does not respect anymore its specification. Such a program is called monitor. A monitor interpret information received from the system as messages (these messages are called events) and propose a diagnosis. The objective of this thesis is to set in place a monitor for a distributed real-time verification of temporal properties. In particular we want our monitor to be able to check up a maximum of properties with a minimum of information. Thus, our tools are designed to work perfectly even if the observation is imperfect, that is to say, even if some events are late or never received. We have also managed to achieve this goal through a highly distributed protocol. To verify the feasibility and effectiveness of our approach, we have established an implementation called Minotor who was found to have very good performance. Finally, we detailed a set of properties, expressed in our formalism, to show it’s expressiveness.

Les réseaux de transport multimodaux modernes sont essentiels pour la durabilité écologique et l’aisance économique des agglomérations urbaines, par conséquent aussi pour la qualité de vie de leurs habitants. D’ailleurs, le bon fonctionnement sur le plan de la compatibilité entre les différents services et lignes est essentiel pour leur acceptation, étant donné que (i) la plupart des trajets nécessitent des changements entre les lignes et que (ii) des investissements coûteux, dans le but de créer des liens plus directs avec la construction de nouvelles lignes ou l’extension de lignes existantes, ne sont pas à débattre. Une meilleure compréhension des interactions entre les modes et les lignes dans le contexte des transferts de passagers est ainsi d’une importance cruciale. Toutefois, comprendre ces transferts est singulièrement difficile dans le cas de situations inhabituelles comme des incidents de passagers et/ou si la demande dévie des plans statistiques à long terme. Ici le développement et l’intégration de modèles mathématiques sophistiqués peuvent remédier à ces inconvénients. À ce propos, la supervision via des modèles prévoyants représente un champ d’application très prometteur, analysée ici. La supervision selon des modèles prévoyants peut prendre différentes formes. Dans le présent travail, nous nous intéressons à l’analyse de l’impact basé sur des modèles de différentes actions, comme des départs en retard de certains véhicules après un arrêt, appliqué sur le fonctionnement du réseau de transport et sa gestion de situations de stress qui ne font pas partie des données statistiques. C’est pourquoi nous introduisons un nouveau modèle, un automate hybride avec une dynamique probabiliste, et nous montrons comment ce modèle profondément mathématique peut prédire le nombre de passagers dans et l’état de fonctionnement du véhicule en question du réseau de transport, d’abord par de simples estimations du nombre de tous les passagers et la connaissance exacte de l’état du véhicule au moment de l’incident. Ce nouvel automate réunit sous un même regard les passagers demandeurs de services de transport à parcours fixes ainsi que les véhicules capables de les assurer. Il prend en compte la capacité maximale et le fait que les passagers n’empruntent pas nécessairement des chemins efficaces, dont la représentation sous la forme d’une fonction de coût facilement compréhensible devient nécessaire. Chaque passager possède son propre profil de voyage qui définit un chemin fixe dans l’infrastructure du réseau de transport, et une préférence pour les différents services de transport sur son chemin. Les mouvements de véhicules sont inclus dans la dynamique du modèle, ce qui est essentiel pour l’analyse de l’impact de chaque action liée aux mouvements de véhicule. De surcroît, notre modèle prend en compte l’incertitude qui résulte du nombre inconnu de passagers au début et de passagers arrivant au fur et à mesure. Comparé aux modèles classiques d’automates hybrides, notre approche inspirée du style des réseaux de Pétri ne requiert pas le calcul de ces équations différentielles à la main. Ces systèmes peuvent être dérivés de la représentation essentiellement graphique d’une manière automatique pour le calcul en temps discret d’une prévision. Cette propriété de notre modèle réduit le risque de précisions faites par des humains et les erreurs qui en résulteraient. Après avoir introduit notre nouveau modèle, nous développons dans ce rapport également quelques éléments constitutifs sous la forme d'algorithmes qui visent les deux types d'impasses qui sont probables d'occurir pendant la simulation faisant un pronostic, c-à-d l'intégration numérique des systèmes de haute dimension d'équations différentielles et l'explosion combinatoire de son état discret. En plus, nous prouvons la faisabilité des calculs et nous montrons les bénéfices prospectifs de notre approche dans la forme de quelques tests simplistes et quelques cas plus réalistes. / Without any doubt, modern multimodal transportation systems are vital to the ecological sustainability and the economic prosperity of urban agglomerations, and in doing so to the quality of life of their many inhabitants. Moreover it is known that a well-functioning interoperability of the different modes and lines in such networked systems is key to their acceptance given the fact that (i) many if not most trips between different origin/destination pairs require transfers, and (ii) costly infrastructure investments targeting the creation of more direct links through the construction of new or the extension of existing lines are not open to debate. Thus, a better understanding of how the different modes and lines in these systems interact through passenger transfers is of utmost importance. However, acquiring this understanding is particularly tricky in degraded situations where some or all transportation services cannot be provided as planned due to e.g. some passenger incident, and/or where the demand for these scheduled services deviates from any statistical long term-plannings. Here, the development for and integration of sophisticated mathematical models into the operation of such systems may provide remedy, where model-predictive supervision seems to be one very promising area of application which we consider here. Model-predictive supervision can take several forms. In this work, we focus on the model-based impact analysis of different actions, such as the delayed departure of some vehicle from a stop, applied to the operation of the considered transportation system upon some downgrading situation occurs which lacks statistical data. For this purpose, we introduce a new stochastic hybrid automaton model, and show how this mathematically profound model can be used to forecast the passenger numbers in and the vehicle operational state of this transportation system starting from estimations of all passenger numbers and an exact knowledge of the vehicle operational state at the time of the incident occurrence. Our new automaton model brings under the same roof, all passengers who demand fixed-route transportation services, and all vehicles which provide them. It explicitly accounts for all capacity-limits and the fact that passengers do not necessarily follow efficient paths which must be mapped to some simple to understand cost function. Instead, every passenger has a trip profile which defines a fixed route in the infrastructure of the transportation system, and a preference for the different transportation services along this route. Moreover, our model does not abstract away from all vehicle movements but explicitly includes them in its dynamics, which latter property is crucial to the impact analysis of any vehicle movement-related action. In addition our model accounts for uncertainty; resulting from unknown initial passenger numbers and unknown passenger arrival flows. Compared to classical modelling approaches for hybrid automata, our Petri net-styled approach does not require the end user to specify our model's many differential equations systems by hand. Instead, all these systems can be derived from the model's predominantly graphical specification in a fully automated manner for the discrete time computation of any forecast. This latter property of our model in turn reduces the risk of man-made specification and thus forecasting errors. Besides introducing our new model, we also develop in this report some algorithmic bricks which target two major bottlenecks which are likely to occur during its forecast-producing simulation, namely the numerical integration of the many high-dimensional systems of stochastic differential equations and the combinatorial explosion of its discrete state. Moreover, we proof the computational feasibility and show the prospective benefits of our approach in form of some simplistic test- and some more realistic use case.

Les convertisseurs de puissance multicellulaires trouvent une place privilégiée dans le contrôle des systèmes de très forte puissance. Dans ce travail de thèse une nouvelle classe de convertisseurs de puissance est étudiée les Convertisseurs Multicellulaires Parallèles (CMP). La topologie de ces convertisseurs repose sur une association de n cellules de commutationinterconnectées par l'intermédiaire d'inductances indépendantes, appelées aussiinductances de liaison. Le CMP permet d'atteindre un courant de sortie égal à n fois le courant d'entrée du convertisseur, l'inconvénient majeur de ce type de convertisseur est le déséquilibrage des courants de branches . Dans le but de réduire et d'économiser le nombre de capteurs, nous avons proposé dans la première partie de la thèse une analyse d'observabilité spécifique à une classe de système dynamique hybride appelée Z(TN)-Observability et synthétisé un observateur hybride en utilisant l'algorithme super twisting. La deuxièmepartie du travail a été consacrée à la synthèse d'une loi de commande pour la régulation des courants de branches. En effet, le régulateur proposé est un régulateur hybride en basant sur la modélisation par réseaux de pétri de l'algorithme de contrôle. Enfin, Les deux parties théoriques sont suivies par une réalisation pratique d'un CMP à trois cellules de commutation pour valider les deux approches proposées. Les résultats expérimentaux nous ont montré les performances de l'observateur et le régulateur de courant et de tension de sortie. / This study deals with observability problems and control of the parallel multicell chopper. In the area of strong currents with high switching frequencies, new structures based on the combination of components have been developed. This type of chopper is a DC/DC static power converter which has an output current equals to n (n is the number of cells) times the source current. After recalling the dynamical equations of the converter, its hybrid dynamical behaviour and properties are highlighted. This particular hybrid system induces new and difficult observability problems, such problem can be tackled by a new observability concept [the Z(TN)-observability]. However, for a large number of switching cells in parallel, the complexity of the system makes it impossible to predict the transient behaviour of the converter and therefore all predimensioning. The main disadvantage of this type of converter is the imbalance branches of current with increasing number of cells. Therefore modelling and control with Petri net is proposed to solve the problems of imbalanced of currents and the voltage output regulation with variation of the load. The authors approaches are attested by several numerical simulations and experimental results considering noisy measurements and load variations.

Nous présentons dans ce travail de thèse des approches pour la spécification et la vérificationdes systèmes temporisés. La première partie concerne une méthode de spécification enutilisant les diagrammes états-transitions pour modéliser un système donné en partant d’unedescription textuelle. Cette méthode guide l’utilisateur pour le développement de la modélisation.Elle comporte plusieurs étapes et utilise des observateurs d’états et des événements afind’engendrer le diagramme états-transitions. Un outil qui implémente les différentes étapes de laméthode de spécification pour une application semi-automatique est présenté. La seconde partieconcerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, cequi permet d’utiliser les méthodes de vérification. Nous prenons en considération dans cette traductionun ensemble important des éléments syntaxiques des diagrammes états-transitions, telsque la concurrence, la hiérarchie, etc. Un outil qui implémente la traduction pour un passageautomatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.La dernière partie concerne l’intégration des contraintes temporelles dans les deuxapproches précédentes. Nous définissons des annotations pour les diagrammes états-transitionsdont nous fournissons la syntaxe et la sémantique. Ces annotations seront ensuite utilisées dansla méthode de spécification et la traduction. Le but est de proposer des annotations faciles àcomprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plusutilisées. / In order to specify and verify timed systems, we present in this thesis approaches using UMLstate machines and coloured Petri nets. Our first approach is a specification method that takesinto account a textual description of the system and generates the corresponding state machinediagram. This method helps a non-expert user to model a system in a structural way. We presenta tool that implements the specification method. Our second approach is the translation of UMLstate machine diagrams to coloured Petri nets diagrams. In this approach we take into account animportant set of UML state machine elements that allows the modelling of concurrent systems,etc. A tool that implements the approach and allows us to automate the translation is beingdeveloped. Finally, the last approach is the integration of time constraints in our specificationmethod and in our translation. We propose a set of annotations to model time in state machinediagrams, and we define the corresponding syntax and semantics.

Dans ce mémoire, nous présentons différentes approches de synthèse de contrôleurs réseaux de Petri en se basant sur la théorie des régions. Cette théorie présente quelques limites dans la synthèse de contrôle. En effet, la synthèse du contrôleur RdP, s’il existe, n’est pas du tout une tâche facile vue sa complexité de calcul et l’explosion combinatoire des états dans le graphe de marquage. De plus, le système linéaire de la théorie des régions à résoudre peut contenir des combinaisons convexes entre ces équations ce qui rend la théorie insoluble pour calculer les superviseurs RdP. Ce travail vise à simplifier la complexité de calcul de la théorie des régions en réduisant le nombre d’équations du système linéaire de la théorie des régions d’une part, et d’autre part en minimisant le temps de calcul des contrôleurs RdP. De nouveaux concepts de coupes minimales et de marquages canoniques ont été introduits afin d’appliquer la théorie des régions sur des zones précises du graphe et non pas sur la totalité du graphe de marquage. Finalement, deux autres nouvelles approches ont été développées pour synthétiser des contrôleurs RdP sans générer le graphe de marquage / In this work, we present different control synthesis approaches based on Petri nets and the theory of regions. This theory has some limitations in supervisory control. Indeed, the design on the PN controller, if it exists, is not an easy task due to the resolution complexity and the combinatorial explosion of states in the generated reachability graph. In addition, the linear system of the theory of regions may contain convex combinations of its equations making the theory insoluble. This work aims to simplify the computational complexity of the theory of regions by reducing the number of equations of the linear system and decreasing the computation time of PN controllers. Consequently, new concepts of minimal cuts and canonic markings are introduced in order to apply the theory of regions on specific zones of the graph and not on the whole reachability graph. Finally, two new approaches are developed to synthesize PN controllers without generating the reachability graph

Le travail présenté dans ce mémoire s'inscrit dans le domaine de la surveillance des systèmes à événements discrets et porte plus particulièrement sur le problème de la détection distribuée de procédés complexes. L'architecture proposée repose sur des sites autonomes et coopératifs de surveillance permettant de surveiller les évolutions du procédé. Ces évolutions, traduisant le fonctionnement attendu (normal) du système ou des situations de défaillance, sont décrites par des chroniques. Chaque chronique est composée d'un ensemble d'événements et d'un ensemble de contraintes temporelles entre ces événements. Trois types de contraintes sont considérés : les contraintes de précédence, les contraintes de types intervalles et les contraintes de type fenêtre d'admissibilité. Une chronique est dite reconnue si toutes les contraintes qui la composent sont vérifiées compte tenu des durées séparant les occurrences des événements la constituant. La distribution du modèle temporel représenté par la chronique induit la distribution de la chronique en sous-chroniques distribuées sur plusieurs sites de surveillance (sous-systèmes). La reconnaissance de l'ensemble des sous-chroniques assure la reconnaissance de la chronique. Cette distribution de la chronique en sous-chroniques permet de mettre en évidence deux types de contraintes : les contraintes locales et les contraintes globales. Les délais de communication ou de transport entre sites sont bornés et sont pris en compte lors de la vérification des contraintes temporelles globales. L'incertitude induite par ces délais engendre une incertitude sur la vérification qui se traduit par une mesure de possibilité associée à la vérification d'une contrainte. Des mécanismes de coopération entre sites de surveillance sont définis. Une modélisation des différents mécanismes développés reposant sur les réseaux de Petri p-t-temporels flous est proposée. Enfin, l'ensemble des travaux est appliqué à la surveillance d'un terminal intermodal de fret.

Le nombre croissant des systèmes électroniques embarqués dans le secteur automobile a considérablement amélioré et diversifié les services rendus par le véhicule. Ces systèmes sont appelés systèmes mécatroniques. Ils intègrent une partie énergétique (mécanique, hydraulique ou électrique) commandée et contrôlée par un calculateur. Leur principal atout est la flexibilité logicielle dont dispose le concepteur pour implémenter de nouvelles fonctions. Toutefois, ceci a contribué à accroître leur complexité et à en diminuer la maîtrise, d'où la nécessité d'effectuer des études de Sûreté de Fonctionnement afin de garantir un bon niveau de sécurité. Par ailleurs, mener de telles études dès la phase de conception permet de diminuer les délais et les coûts de conception en détectant et en corrigeant au plus tôt les erreurs de conception. Actuellement, les études de sécurité prévisionnelle des systèmes automobiles sont réalisées par la méthode des Arbres de Défaillance. Or cette méthode est statique et ne permet pas de prendre en compte les phénomènes temporels liés à leur dynamique de fonctionnement et à leur aspect hybride. C'est dans ce contexte que des recherches sont menées en collaboration entre le groupe PSA Peugeot Citroën et le LAAS visant à développer une méthodologie d'aide à la conception de systèmes mécatroniques sûrs de fonctionnement. Mon projet de thèse se focalise sur l'analyse qualitative de la sécurité des systèmes mécatroniques en vue de l'obtention des scénarios redoutés. La connaissance de ces scénarios permet d'évaluer leurs probabilités d'occurrence et de valider les lois de reconfiguration pour orienter le choix des concepteurs quant aux différents types d'architectures possibles proposés pour le système. Nous avons développé une méthode de recherche des scénarios redoutés basée sur la modélisation préalable d'un système mécatronique sous la forme d'un Réseau de Petri et d'un ensemble d'équations différentielles. Cette modélisation hybride présente l'avantage de séparer clairement les aspects discrets et continus. Ceci nous permet une analyse logique (fondée sur la logique Linéaire) des causalités résultant des changements d'états. Grâce à cette analyse, il est possible à partir d'un état redouté de remonter les chaînes de causalité et de mettre ainsi en évidence tous les scénarios possibles conduisant à une situation critique. Chaque scénario est donné sous la forme d'un ordre partiel entre les événements nécessaires à l'apparition de l'état redouté. L'originalité de notre approche est qu'elle n'implique pas une énumération brutale et globale de tous les états accessibles du système. Au contraire elle permet de se focaliser sur le voisinage de l'état redouté en faisant une énumération locale d'états partiels. Autrement dit, nous ne considérons que les états des composants directement impliqués dans l'apparition de l'état redouté. Nous avons enfin élaboré un algorithme automatisant la recherche des scénarios redoutés et nous l'avons appliqué sur deux exemples simples de systèmes mécatroniques.

En logique classique, la formalisation du fonctionnement des réseaux de Petri (RdP) se heurte à la pérennité de la vérité. En logique modale, elle impose la construction préalable du graphe des marquages accessibles. A contrario, la logique linéaire (LL) fondée par Girard permet de formaliser directement par des séquents prouvables purement propositionnels les relations d'accessibilité dans les RdP : toute transition apparaît comme une implication linéaire disponible ad libitum entre les propositions traduisant ses marquages d'entrée et de sortie. Pour approfondir cette formalisation, nous définissons comme primitives en LL les notions de ressource, d'action et de consommabilité/productibilité, analogues mais distinctes de celles de proposition, de déduction et de vérité/fausseté en logique classique. Nous développons une interprétation concrète pour tous les connecteurs linéaires en cohérence avec leurs propriétés syntaxiques. Nous présentons le connecteur « par » comme un opérateur de cumul disjoint d'exemplaires de ressources (dual du connecteur « fois » de cumul conjoint) et la négation linéaire « nil » comme un inverseur du sens du temps. Cette concrétisation montre les limites des formalisations existantes des RdP en LL ; nous les généralisons en traduisant chaque transition par une implication linéaire ordinaire, traitée comme une ressource périssable, dont tout exemplaire consommé correspond à une occurrence de franchissement. Ainsi, nous apportons une expression logique aux aspects primordiaux du fonctionnement des RdP : nous démontrons qu'une relation d'accessibilité par séquence de transitions équivaut à un séquent prouvable et que l'équation fondamentale est l'expression algébrique d'un corollaire du critère d'équilibrage en LL. Grâce à la combinatoire de tous les connecteurs linéaires, notre approche ouvre des perspectives d'analyse de relations complexes d'accessibilité comme celles de reprise après défa illance dans un système industriel.

Les erreurs humaines et les interruptions sont des phénomènes courants mais négligés, voire ignorés, dans le processus de développement des systèmes interactifs. En outre, leur automatisation massive n'a pas éliminé erreurs et interruptions, mais en a accentué le caractère critique. Ce mémoire a pour objet l'amélioration de la fiabilité des systèmes homme-machine par la prise en compte explicite des erreurs et des interruptions dans la pratique de l'Ingénierie de l'Interaction Homme-Machine. Nous appliquons notre étude au cas exigeant des systèmes critiques automatisés et notamment aux systèmes aéronautiques, pour lesquels les erreurs humaines et les interruptions ont une importance décisive. Dans la première partie du mémoire, dédiée aux concepts, nous présentons une revue des recherches sur l'automatisation et sur l'analyse des erreurs humaines telle que l'envisage la psychologie cognitive. A notre tour, nous proposons le concept de singularité comme notion pivot aux phénomènes d'erreur et d'interruption. Nous en fournissons un modèle qui explicite les activités mentales en relation avec la détection et la correction de singularité. La seconde partie du mémoire a trait à l'expression formelle des singularités dans le processus de développement d'un système interactif. Après une revue des formalismes et des notations utilisés en Interaction Homme-Machine, nous retenons MAD, UAN et les réseaux de Petri pour leurs qualités et leur usage complémentaires. Pour chacun, nous proposons les extensions nécessaires à l'expression des singularités. Nous fournissons également les règles de traduction de ces extensions entre les trois formalismes retenus, évitant ainsi la perte de conformité au cours du processus de développement d'un système.

Cette thèse traite du problème de la vérification de systèmes ayant un nombre infini d'états. Ces systèmes peuvent être décrits par plusieurs formalismes tels que des algèbres de processus ou des automates finis munis de structures de données non-bornées (automates à pile, réseaux de Petri ou systèmes à files). Dans une première partie de la thèse nous nous intéressons à la caractérisation de classes de systèmes infinis et de propriétés pour lesquels le problème de vérification est décidable. Nous considérons d'abord la complexité de la vérification du mu-calcul linéaire pour les réseaux de Petri. Ensuite, nous définissons des logiques temporelles qui permettent d'exprimer des propriétés non-régulières comportant des contraintes linéaires sur le nombre d'occurrences d'événements. Ces logiques sont plus expressives que les logiques utilisées dans le domaine. Nous montrons en particulier que le problème de la vérification d'une logique qui est plus expressive que le mu-calcul linéaire est décidable pour des classes de systèmes infinis telles que les automates à pile et les réseaux de Petri. Une deuxième partie de la thèse est consacrée aux systèmes communicant par files d'attente, dont le problème de vérification est en général indécidable. Nous appliquons le principe de l'analyse symbolique à ces systèmes. Nous proposons des structures finies qui permettent de représenter et de manipuler des ensembles infinis de configurations de tels systèmes. Ces structures permettent de calculer l'effet exact d'une exécution répétée de tout circuit dans le graphe de transitions du système. Ainsi, chaque circuit peut être considéré comme une nouvelle "transition" du système. Nous utilisons ce résultat pour accélérer le calcul de l'ensemble des configurations atteignables d'un système afin d'augmenter les chances de terminaison de ce calcul.