Les automates temporisés avec mises à jour.

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

Cette thèse propose une nouvelle approche pour la synthèse de valeurs temporelles dans les systèmes temporisés. Notre approche est basée sur la méthode inverse suivante : à partir d’une instance de référence des paramètres, nous synthétisons une contrainte sur les paramètres, garantissant le même comportement que pour l’instance de référence, abstraction faite du temps. Il en résulte un critère de robustesse pour le système. En itérant cette méthode sur des points dans un domaine paramétrique borné, nous sommes alors à même de partitionner l’espace des paramètres en bonnes et mauvaises zones par rapport à une propriété à vérifier. Ceci nous donne une cartographie comportementale du système. Cette méthode s’étend aisément aux systèmes probabilistes. Nous présentons également des variantes de la méthode inverse pour les graphes orientés valués et les processus de décision markoviens. Parmi les prototypes implémentés, IMITATOR II implémente la méthode inverse et la cartographie pour les automates temporisés. Ce prototype nous a permis de synthétiser de bonnes valeurs pour les paramètres temporels de plusieurs études de cas, dont un modèle abstrait d’une mémoire commercialisée par le fabricant de puces STMicroelectronics, ainsi que plusieurs protocoles de communication. / This thesis proposes a novel approach for the synthesis of delays for timed systems, in particular in the framework oftimed automata, a model for verifying real-time systems. Our approach relies on the following inverse method: given a reference valuation of the parameters, we synthesize a constraint on the parameters, guaranteeing the same timeabstract linear behavior as for the reference valuation. This gives a criterion of robustness to the system. By iterating this inverse method on various points of a bounded parameter domain, we are then able to partition the parametric space into good and bad zones, with respect to a given property one wants to verify. This gives a behavioral cartography of the system. This method extended to probabilistic systems allows to preserve minimum and maximum probabilities of reachability properties. We also present variants of the inverse method for directed weighted graphs and Markov Decision Processes. Several prototypes have been implemented; in particular, IMITATOR II implements the inverse method and the cartography for timed automata. It allowed us to synthesize parameter values for several case studies such as an abstract model of a memory circuit sold by the chipset manufacturer ST-Microelectronics, and various communication protocols.

La vérification est maintenant une branche très connue des sciences informatiques. Elle est cruciale lorsque l'on a affaire à des programmes informatiques dans des systèmes automatiques : on veut vérifier si un système donné est correct et s'il satisfait des propriétés nécessaires à son bon fonctionnement. Une façon d'analyser ces systèmes se fait par la modélisation mathématique. La question est alors : peut-on vérifier si le modèle satisfait les propriétés requises ? C'est ce que l'on appelle le problème du model-checking. Plusieurs modèles ont été étudiés dans la littérature. Nous portons notre intérêt sur des modèles qui peuvent mêler des aspects temporels et des aspects probabilistes. Dans cette thèse, nous étudions donc le modèle des automates temporisés et stochastiques (ATS). Les contributions de ce document sont divisées en deux parties. Tout d'abord, nous étudions les problèmes de model-checking qualitatifs et quantitatifs des ATS. Les ATS sont, en particulier, des systèmes probabilistes généraux et avec de tels modèles, on est intéressé par des questions du type : « Une propriété est-elle satisfaite, au sein d'un modèle donné, avec probabilité 1 ? » (qualitatif) ou bien « Peut-on calculer une approximation de la probabilité que le modèle satisfait une propriété donnée ? » (quantitatif).Nous étudions ces questions dans des systèmes probabilistes généraux en utilisant, entre autres, la notion de decisiveness utilisée dans les chaînes de Markov infinie dans le but d'obtenir d'importants résultats qualitatifs et que nous étendons ici dans notre contexte plus général. Nous prouvons plusieurs résultats pour les problèmes de model-checking qualitatifs et quantitatifs de ces systèmes probabilistes, certains d'entre eux étant des extensions de travaux antérieurs sur les chaînes de Markov, d'autres étant nouveaux, et nous montrons comment l'on peut appliquer ces résultats sur des sous-classes des ATS. Nous étudions ensuite la vérification compositionnelle des ATS. En général, un système est le résultat de plusieurs plus petits systèmes fonctionnant ensemble. La vérification compositionnelle permet alors de réduire l'analyse de gros systèmes aux analyses des plus petits systèmes qui le composent. Il est donc crucial d'avoir une bonne structure compositionnelle au sein des modèles mathématiques, et cela manque aux ATS. Dans cette thèse, nous définissons un opérateur de composition pour les ATS. Nous faisons d'abord l'hypothèse que les ATS composés fonctionnent complètement indépendamment l'un de l'autre, c'est-à-dire les ATS ne communiquent pas entre eux. Nous prouvons que notre définition satisfait bien cette hypothèse d'indépendance. Un tel opérateur de composition n'est pas très intéressant puisque, généralement, les systèmes interagissent entre eux. Mais c'est une première étape nécessaire. Nous introduisons donc le nouveau modèle des ATS interactifs (ATSI) qui vont permettre des interactions entre les systèmes. Nous définissons un opérateur de composition dans les ATSI qui va rendre possible des synchronisations entre les systèmes et qui est construit sur la précédente composition dans les ATS. Nous finissons cette thèse par l'identification d'une sous-classe de ATSI dans laquelle tous les résultats qualitatifs et quantitatifs fournis dans cette thèse peuvent être appliqués, et qui est donc accompagnée d'une bonne structure compositionnelle au sein du modèle. / Verification is now a well-known branch in computer science. It is crucial when dealing with computer programs in automatic systems: we want to check if a given system is correct and satisfies some specifications that should be met. One way to analyse those systems is to model them mathematically. The question is then: can we check if the model satisfies the required specifications ? This is called the model-checking problem. Several models have been studied in the literature. We have an interest for models that can mix both timing and randomized aspects. In this thesis we thus study the stochastic timed automaton model (STA). The contributions of this document are twofold. First, we study the qualitative and quantitative model-checking problems of STA. STA are, in particular, general probabilistic systems and with such model, one is thus interested in questions like « Is a property satisfied, within a given model, with probability 1 ? » (qualitative) or « Can we compute an approximation of the probability that the model satisfies a given property ? » (quantitative).We study those questions for general stochastic systems using, amongst other, the notion of decisiveness used in infinite Markov chains in order to get strong qualitative and quantitative results, and that we extend here in or more general context. We prove several results for the qualitative and quantitative model-checking problems of those probabilistic systems, some of them being extensions of previous work on Markov chains, others being new, and we show how it can be applied to subclasses of STA. Then we study the compositional verification in STA. In general, a system is the result of several smaller systems working together. Compositional verification allows then one to reduce the analysis of a big system to the analyses of the smaller systems which compose it. It is then crucial to have a good compositional framework in mathematical models, and this lacks in STA. In this thesis, we define an operator of composition for STA. We first make the assumption that the STA composed run completely independently from each other, i.e. they do not communicate between them. We prove that our definition satisfies indeed this independence assumption. Such an operator of composition is not very interesting as in general, systems do communicate. But it is a necessary first step. We then introduce the new model of interactive STA (ISTA) that will allow for interactions between the systems. We define an operator of composition in ISTA that will make synchronisations possible between the systems and that is built on the previous composition in STA. We end this thesis with the identification of a subclass of ISTA in which all the qualitative and quantitative results provided in this thesis can be applied, and which thus comes with the nice compositional framework defined in the model.

Dans cette thèse, nous nous intéressons au calcul d'ordonnanceurs pour les systèmes hybrides. En fait, nous considérons deux sous-classes des systèmes hybrides, les systèmes temps-réels où des tâches doivent se partager l'accès à une ressource commune, et les systèmes à commutations où un choix doit être fait sur les dynamiques à choisir en fonction d'objectifs à atteindre. Dans la première partie de cette thèse, nous nous intéressons aux problèmes d'ordonnancement et prenons comme étude de cas l'ordonnancement de tâches périodiques sur des architectures multiprocesseurs. Nous nous intéressons plus particulièrement à déterminer si l'on peut modifier certaines valeur des paramètres du système tout en respectant les contraintes temporelles sans changer d'ordonnanceur. La méthode inverse permet de prouver de manière formelle la robustesse des systèmes temporisés paramétriques. Nous introduisons une méthode de réduction du nombre d'états nécessaire à la vérification. Cette réduction nous permet de traîter des études de cas intéressantes telle que celle proposée par Astrium EADS pour le lanceur Ariane 6. Nous montrons également comment la Cartographie Comportementale, une extension de la méthode inverse, permet de trouver la zone de l'espace des paramètres où l'on a l'existence d'un ordonnancement satisfaisant les contraintes temporelles. Nous comparons cette approche avec une méthode analytique pour montrer l'intérêt de notre approche. Dans la seconde partie de cette thèse, nous nous intéressons au contrôle de systèmes affines à commutation. Ces systèmes sont gouvernés par une famille d'équations différentielles linéaires et le contrôleur peut choisir laquelle va gouverner le système pendant le prochain pas de temps. Dans ce cadre, le contrôle peut être vu comme l'ordonnancement des dynamiques que le système va prendre. Le choix de la dynamique peut se faire pour des objectifs de stabilité ou d'accessibilité. Nous proposons une nouvelle méthode qui calcule un contrôleur dont la stratégie est la même pour des ensembles denses de points. Notre méthode utilise le calcul en avant, souvent préférable au calcul à rebours pour les systèmes contractants. Nous montrons que, sous certaines conditions, le système contrôlé évolue vers un comportement limite. Nous appliquons notre méthode sur plusieurs études de cas issues de la littérature ainsi qu'un exemple réel, un prototype de convertisseur de tension multiniveaux. Enfin, nous montrons que notre méthode s'étend aux systèmes comportant des perturbations ainsi qu'aux systèmes non linéaires. / In this thesis, we are interested in designing schedulers for hybrid systems. We consider two specific subclasses of hybrid systems, real-time systems where tasks are competing for the access to common resources, and sampled switched systems where a choice has to be made on dynamics of the system to reach goals. Scheduling consists in defining the order in which the tasks will be run on the processors in order to complete all the tasks before a given deadline. In the first part of this thesis, we are interested in the scheduling of periodic tasks on multiprocessor architectures. We are especially interested in the robustness of schedulers, i.e., to prove that some values of the system parameters can be modified, and until what value they can be extended while preserving the scheduling order and meeting the deadlines. The Inverse Method can be used to prove the robustness of parametric timed systems. In this thesis, we introduce a state space reduction technique which allows us to treat challenging case studies such as one provided by Astrium EADS for the launcher Ariane 6. We also present how an extension of the Inverse Method, the Behavioral Cartography, can solve the problem of schedulability, i.e., finding the area in the parametric space in which there exists a scheduler that satisfies all the deadlines. We compare this approach to an analytic method to illustrate the interest of our approach In the second part of this thesis, we are interested in the control of affine switched systems. These systems are governed by a finite family of affine differential equations. At each time step, a controller can choose which dynamics will govern the system for the next time step. Controlling in this sense can be seen as a scheduling on the order of dynamics the system will have to use. The objective for the controller can be to make the system stay in a given area of the state space (stability) or to reach a given region of the state space (reachability). In this thesis, we propose a novel approach that computes a scheduler where the strategy is uniform for dense subsets of the state space. Moreover, our approach only uses forward computation, which is better suited than backward computation for contractive systems. We show that our designed controllers, systems evolve to a limit cyclic behavior. We apply our method to several case studies from the literature and on a real-life prototype of a multilevel voltage converter. Moreover, we show that our approach can be extended to systems with perturbations and non-linear dynamics.

Les systèmes digitaux jouent un rôle croissant dans le bon fonctionnement de notre société.Au delà de la grande diversité de leur domaines d'utilisations, on confie aujourd'hui destâches importantes à des algorithmes. Déjà largement utilisés dans des domaines aussi délicatque le transport, la chirurgie ou l'économie, il est aujourd'hui de plus en plus question defaire de la place aux systèmes digitaux dans les domaines sociaux et politiques :vote électronique, algorithmes de sélection, profilage électoraldotsPour les tâches confiées à des algorithmes, la responsabilité est déplacées de l'exécutantvers les concepteurs, développeurs et testeurs de ces algorithmes. Il incombe aussi auxchercheurs qui étudient ces algorithmes de proposer des techniques de vérifications fiablequi pourront être utilisées à tous les niveaux : conception, développement et test.Les méthodes de vérifications formelles donnent des outils mathématiques pourprévenir des erreurs à chaque niveaux. Parmi elle, le diagnostic d'erreur consiste en lacréation d'un diagnostiqueur basé sur un modèle formel du système à vérifier.Le diagnostiqueur est exécuté en parallèle du système qu'il doit surveiller et prévientun contrôleur si il détecte un comportement dangereux du système.Pour les systèmes modélisés par des automates temporisés, il n'est pas toujours possiblede construire un diagnostiqueur sous la forme d'un autre automate temporisé. En effetles automates temporisés, introduits par cite{AD94} dans les années 90 et largementétudiés et utilisés depuis pour modéliser des systèmes avec contraintes temporelles,ne sont pas déterminisable. Une machine plus puissante qu'un automate temporisé peutcependant être utilisée pour construire le diagnostiqueur d'un automate temporisé commele montre cite{Tripakis02}. L'aboutissement de ce travail de thèse est la constructionautomatique d'un diagnostiqueur pour les automates temporisés à une horloge.Ce diagnostiqueur, dans le même esprit que celui de cite{Tripakis02}, est une machineplus puissante qu'un automate temporisé. La partie~I du manuscrit introduit un cadreformel pour ce type de machine et plus généralement pour la modélisation et ladéterminisation de systèmes quantitatifs. Y est introduit le modèle des automates surstructures temporisés, qui apporte un nouveau point de vue sur la manière de modéliserles systèmes avec variables quantitatives. La partie~II étudie le problème de ladéterminisation des automates sur structures temporises, et plus spécifiquement celuides automates temporisés qui peuvent se traduire dans ce cadre nouveau cadre formel.La partie~III montre comment utiliser les automates sur structure temporisés pourconstruire de manière générique un diagnostiqueur pour les automate temporisés à unehorloge. Cette technique est implémentée dans un outils, DOTA , et comparée à lamachine construite par cite{Tripakis02}. / Digital system are now part of our society. They are used in a wide range of domainsand in particular they have to handle delicate tasks. Already used in domainssuch as transportation, surgery or economy, we speak now of using digital systemsfor social or political matters : electronic vote, selection algorithms, electoralprofilingdots For task handled by algorithm, the responsibility is moved from theexecutioner to the designer, developer and tester of those algorithms. It is alsothe responsibility of computer scientists who study those algorithms to proposereliable techniques of verification which will be applicable in the design, thedevelopment or the testing phase. Formal verification methods provide mathematicaltools to prevent executions error in all phases. Among them, fault-diagnosis consiston the construction of a diagnoser based on a formal model of the system we aim tocheck. The diagnoser runs in parallel with the real system and emit a warning anytime it detect a dangerous behavior. For systems modeled by timed automata, it isnot always possible to construct a timed automaton to diagnose it. Indeed timed automata,introduce in the nineties by cite{AD94} and widely studied and used since to modeltimed systems, are not determinizable. A machine, more powerful than a timed automaton,can still be used to construct the diagnoser of a timed automaton as it is done incite{Tripakis02}. This thesis work aim at constructing a diagnoser for any one-clocktimed automata. This diagnoser is constructed with the help of a machine more powerfulthan timed automata, following the idea of cite{Tripakis02}. Part~I of this thesisintroduce a formal framework for the modeling of quantitative systems and the study oftheir determinization. In this framework we introduce automata on timed structures,the model used to construct the diagnoser. Part~II study the determinization problemof automata on timed structures, and particularly the one of timed automatadeterminization in this framework. Part~III illustrate how automata on timed structurescan be used to construct in a generic way a diagnoser for one clock timed automata.This technique is implemented in a tool, DOTA , and is compared to the technique usedin cite{Tripakis02}.

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

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.

Les automates temporisés sont un formalisme qui permet de modéliser, vérifier, et synthétiser des systèmes temps-réels. Ils sont dotés d’une sémantique abstraite et mathé- matique, qui permet de formaliser et résoudre plusieurs problèmes de vérification et de synthèse. Cependant, les automates temporisés sont utilisés pour concevoir des modèles, plutôt que décrire des systèmes temps-réels entiers. Ainsi, une fois la phase de conception terminée, il reste à déterminer si les comportements du modèle correspondent à ceux d’un vrai système. Une étape importante de l’implémentation consiste à s’assurer de la robustesse du système. On considère une notion de robustesse sur les automates tem- porisés qui exige que les comportements soient préservés quand le modèle est sujet à des perturbations bornées. Dans cette thèse, plusieurs approches sont étudiées : Dans l’analyse de robustesse, on se demande si un automate temporisés donné préserve ses com- portements sous divers types de perturbations, et on cherche à calculer un majorant sur les perturbations tolérées. La synthèse robuste s’intéresse au calcul d’une loi de contrôle (ou une stratégie) qui guide le système, et tolère des perturbations d’une magnitude calculable. Enfin, dans l’implémentation robuste, on s’intéresse à transformer automatiquement un modèle donné pour le rendre robuste, tout en préservant ses comportements. Plusieurs modèles de perturbations sont considérés : erreurs de mesure de temps (élargissement de gardes), élimination des comportements limites (contraction de gardes), et la restriction du domaine du temps aux valeurs discrètes. On formalise également les problèmes de synthèse robuste comme des jeux entre le contrôleur et un environnement qui perturbe systèmatiquement tout délai choisi par une quantité bornée. Ces problèmes sont étudiés pour les automates temporisés, ainsi que leurs extensions- les jeux temporisés, et les automates et jeux temporisés pondérés. Plusieurs algorithmes d’analyse de robustesse parametrée contre l’élargissement de gardes et la contraction de gardes sont proposés. Deux variantes de la sémantique de jeu pour le problème de synthèse robuste sont également étudiées pour les automates temporisés et leurs extensions. Un logiciel d’analyse de robustesse contre la contraction de gardes, ainsi que des résultats expérimentaux sont présentés. Le problème de l’implémentation robuste est étudié dans deux contextes différents. Tous les algorithmes calculent également un majorant sur les perturbations que le modèle donné est capable de tolérer. / Timed automata are a formalism to model, verify, and synthesize real-time systems. They have the advantage of having an abstract mathematical semantics, which allow formalizing and solving several verification and synthesis problems. However, timed automata are intended to design models, rather than completely describe real systems. Therefore, once the design phase is over, it remains to check whether the behavior of an actual implementation corresponds to that of the timed automaton model. An important step before implementing a system design is ensuring its robustness. This thesis considers a notion of robustness that asks whether the behavior of a given timed automaton is preserved, or can be made so, when it is subject to small perturbations. Several approaches are considered: Robustness analysis seeks to decide whether a given timed automaton tolerates perturbations, and in that case to compute the (maximum) amount of tolerated perturbations. In robust synthesis, a given system needs to be controlled by a law (or strategy) which tolerates perturbations upto some computable amount. In robust implementation, one seeks to automatically transform a given timed automaton model so that it tolerates perturbations by construction. Several perturbation models are considered, ranging from introducing error in time measures (guard enlargement), forbidding behaviors that are too close to boundaries (guard shrinking), and restricting the time domain to a discrete sampling. We also formalize robust synthesis problems as games, where the control law plays against the environment which can systematically perturb the chosen moves, by some bounded amount. These problems are studied on timed automata and their variants, namely, timed games, and weighted timed automata and games. Algorithms for the parameterized robustness analysis against guard enlargements, and guard shrinkings are presented. The robust synthesis problem is studied for two variants of the game semantics, for timed automata, games, and their weighted extensions. A software tool for robustness analysis against guard shrinkings is presented, and experimental results are discussed. The robust implementation problem is also studied in two different settings. In all algorithms, an upper bound on perturbations that the given timed automaton tolerates can be computed.

Ce travail s'inscrit dans la continuité de l'étude du langage de description de systèmes AltaRica. Ce langage, développé au Labri, permet de modéliser des systèmes réels de manière hiérarchique. L'objectif de la thèse est d'introduire le temps quantitatif dans le but de concevoir des systèmes temps réel, c'est à dire des systèmes assujettis à des contraintes temporelles.<br />Deux extensions du langage sont proposées : une version temporisée et une hybride. Ces extensions respectent les caractéristiques du langage initial et conservent les aspects de hiérarchie, de synchronisation, de partage de variables et de priorité statique. En outre, afin d'améliorer les descriptions temps réel, de nouveaux opérateurs de modélisation, comme l'urgence et les priorités temporelles, ont été ajoutés. Nous obtenons ainsi un langage hiérarchique de haut niveau de modélisation de systèmes temps réel. <br />Une étude formelle complète a été menée sur la sémantique du langage, le pouvoir d'expression des langages AltaRica temps réel et des moyens de traductions automatiques vers des modèles classiques existants. Ces algorithmes reposent sur la notion de mise à plat de modèle, i.e. réécrire le modèle sans sous composant.<br />Enfin, le langage temporisé est implanté dans un prototype qui étant donné un modèle le met à plat puis le traduit en automate temporisé. Ainsi, certains systèmes réels ont pu être modélisés puis des propriétés ont été vérifiées à l'aide du model checker UPPAAL.