Ce mémoire de thèse prèsente une approche pour la surveillance des systèmes à événements discrets commandés. L'étude se restreint aux défauts interruptibles : intermittents et permanents. Le comportement acceptable de ces systèmes est introduit afin d'accroître la disponibilité des systèmes commandés. Ce comportement présente une tolérance aux défauts intermittents. Une démarche de construction du système de surveillance est présentée. Nous modélisons, dans un premier temps, le comportement du système sujet aux défauts interruptibles par un automateà chronomètres. Nous appliquons, dans un deuxième temps, une procédure de synthèse à cet automate. Cette procédure est basée aux opérateurs d'analyse en avant et en arriérer de l'automate. Un nouveau modèle appelé réseaux de Petri à chronomètres post- et Pré-initialisés est également présenté. Ce modèle général du RdP a été utilisé, dans le cadre de ce mémoire, pour modéliser le comportement des systèmes sujets aux défauts interruptibles. L'implémentation de notre méthode de surveillance se fait par un automate programmable industriel. Pour ce faire, le système de surveillance étant sous la forme d'un automate àchronomètres est traduit structurellement en programme SFC.

<p>Les travaux présentés portent sur l'étude de méthodes de vérification paramétrée des systèmes temps réels. La motivation pour ces recherches est de proposer des méthodes formelles à appliquer sur des systèmes dont les spécifications ne sont pas encore complètes. Des paramètres sont donc introduits dans les modèles utilisés afin de donner des degrés de liberté à la modélisation. Le but est alors de guider la conception du système en déterminant des valeurs satisfaisantes pour les paramètres.</p> <p>Nous nous sommes focalisé sur les paramètres temporels qui sont en général parmi les plus complexes à définir. Nous avons ainsi défini le modèle des réseaux de Petri à chronomètres paramétrés.</p> <p>Dans une première approche, nous étendons les méthodes d'analyse classiquement utilisées dans les réseaux de Petri temporels. L'espace d'états du modèle paramétré est ainsi représenté par le graphe des classes d'états paramétrées. Cela nous permet de proposer des semi-algorithmes de model-checking paramétré avec lesquels nous vérifions des formules de logique TCTL paramétrées.</p> <p>Dans une seconde approche, nous étudions les méthodes qui préservent le parallélisme des réseaux de Petri. L'intérêt est de limiter l'explosion combinatoire qui apparaît lors de l'analyse de systèmes distribués, en particulier avec des modèles paramétrés. Nous proposons pour cela une méthode de dépliage temporel paramétré. Ce dépliage est a priori infini, mais nous proposons de l'utiliser pour résoudre un problème de supervision. La construction du dépliage est alors guidée par des observations finies, et nous extrayons les explications de ces observations, ainsi que les contraintes sur les paramètres qu'elles induisent.</p>

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit

Cette thèse traite de la vérification formelle de systèmes critiques où la correction du système dépend du respect des contraintes temporelles. La première partie étudie la modélisation et la vérification formelle par model-checking de systèmes temps réel dans le contexte de l’industrie aéronautique et spatiale. La deuxième partie décrit notre méthode d’exploitation des symétries pour les réseaux de Petri temporels. Nous définissons un opérateur de composition symétrique pour la construction de réseaux. Puis nous proposons des solutions pour la construction d’espaces d’états quotients par la relation d’équivalence induite par les symétries. Notre méthode s’applique aux réseaux de Petri, temporels ou non. A notre connaissance il s’agit de la première méthode applicable aux réseaux de Petri temporels. Des résultats expérimentaux encourageants sont présentés. / This thesis deals with formal verification of critical systems where the system’s correction depends on compliance with time constraints. The first part studies the formal modeling and verification by model-checking of realtime systems in the context of the aerospace industry. The second part describes our method for symmetry reduction of Time Petri Net. We define a symmetric composition operator for building Net. Then we present our solution for construction of quotients of the state spaces by the equivalence relation induced by symmetries. Our method applies to Petri nets, temporal or not, but to our knowledge this is the first methodology for Time Petri Nets. Encouraging experimental results are presented.

Cette thèse porte sur le diagnostic des défauts dans des Systèmes à Evènements Discrets (SED) pour lesquels l’occurrence des événements est soumise à des contraintes temporelles. Les domaines d’application potentiels sont nombreux et variés allant de la production manufacturière aux systèmes de transport en passant par les réseaux de communication et les systèmes d’information. La complexité croissante de ces systèmes nécessite l’élaboration de méthodes de surveillance de plus en plus efficaces et performantes pour garantir leur sécurité, leur disponibilité ainsi que le maintien de leurs propriétés dans le temps. Les réseaux de Petri Stochastiques Temporisés Partiellement Observés (RdPSTPO) sont utilisés pour modéliser le système ainsi que les défauts qui peuvent l’affecter. L’étude concerne particulièrement les défauts qui se traduisent par la violation des contraintes temporelles. Une exploitation pertinente des informations temporelles, en vue du diagnostic, constitue la contribution majeure de la thèse. En effet, une meilleure utilisation de ces informations permet de discerner avec précision les différents comportements qui expliquent les mesures. De plus, la probabilité d’occurrence des défauts est calculée en fonction des dates des mesures collectées. Deux approches sont développées : la première est dédiée aux défauts ponctuels et la seconde aux dérives lentes dans les systèmes cycliques. / This PhD thesis deals with the fault diagnosis of Discrete Event Systems (DES) for which the occurrence of events is constrained by temporal specifications. The domain of application is large and varied ranging from manufacturing systems to transportation systems, communication networks and information systems. The increasing complexity of these systems requires the development of effective and efficient monitoring methods to ensure their security, availability and the maintenance of their properties over the time. For that purpose, Partially Observed Stochastic Timed Petri Nets (POSTPN) are used to model the system and the different faults that may affect it. The study is particularly concerned with faults that result after the violation of temporal constraints. Our main contribution in this thesis is the relevant exploitation of the timed information for the fault diagnosis. In fact, a better use of these temporal informations allow to discern with precision the different behaviors that are consistent with the measurements. In addition, the probability of faults occurrence is evaluated according to the dates of collected measurements. Two approaches are developed : the first one is used for single faults and the second one for slow drifts in cyclical systems.

L'Ingénierie Système (IS) est une méthodologie pluridisciplinaire de conception et de mise en oeuvre des systèmes complexes. La maîtrise de la Sûreté de Fonctionnement est un processus essentiel de l'IS et, dans sa poursuite, le recours à des méthodes formelles telles que le model checking se heurte généralement à des diffcultés d'utilisation. Dans cette thèse Cifre, effectuée en collaboration avec l'IRCCyN et Sodius, nous avons cherché à concevoir un outil de vérification formelle d'architectures fonctionnelles qui soit immédiatement utilisable dans des démarches de conception d'IS. Dans ce but, nous transformons des modèles et des propriétés comportementales haut niveau vers des équivalents bas niveau sur lesquels sont effectuées les vérifications formelles, le résultat étant présenté en termes haut niveau. Plus particulièrement, nous avons choisi comme modèles d'entrée les diagrammes EFFBDs : ils constituent un outil de modélisation largement utilisé en IS et adapté aux contraintes du model checking. Nous en avons établi la syntaxe et la sémantique formelles ; nous avons alors pu décrire une transformation vers les réseaux de Petri temporels (TPNs) dont nous avons prouvé qu'elle préserve le comportement temporel des modèles. Parallèlement, nous avons décrit une logique temporelle quantitative adaptée aux EFFBDs et sa traduction vers une logique correspondante sur les TPNs; nous avons alors pu établir la complexité de son model checking. Ces différents résultats théoriques nous ont ensuite permis de réaliser un outil de simulation enfin de vérification d'architectures fonctionnelles et dysfonctionnelles (c.-à-d. modélisant des fonctions défaillantes), déployé et utilisé industriellement.

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit / The introduction of new European standards for railway safety, coupled with an increasing use of software technology changes the method of development of critical railway systems. Indeed, new systems have to be at least as good as the previous ones. Therefore the appropriate safety level of critical systems has to be proved in order to obtain the necessary approval from the authorities. Accordingly a high level of reliability and correctness must be reached by the use of mathematical proofs and then formal methods. We focus on the treatment of the temporal requirements in the level crossing case study which is modelled with p-time Petri nets, and on the translation of this model in a more formal way by using the B method. This paper introduces a methodology to analyse the safety of timed discrete event systems. First, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Then we aim at describing a process identified as a solution of the system functioning. This method consists in exploring all the possible behaviours of the system by means of the construction of state classes. Finally, we check if the proposed process corresponds to the requirements model previously built.Our case-study is the level crossing, a critical component for the safety of railway systems

Ce travail est consacré à la problématique du suivi des systèmes répartis temps réel. Plus précisément, il se concentre sur les aspects formels de la supervision basée sur des modèles ainsi que sur les problèmes qui lui sont liés. Dans la première partie du travail, nous présentons les propriétés de base de deux modèles formels bien connus utilisés pour la modélisation de systèmes répartis : les réseaux d'automates temporisés et les réseaux de Petri temporels. Nous montrons que le comportement de ces modèles peut être représenté par les procédés dits de branchement. Nous introduisons également les éléments conceptuels clés du système de surveillance. La deuxième partie du travail est consacrée à la question des dépliages avec contraintes qui permettent le suivi des relations causales entre les événements dans un système réparti. Ce type de structure peut reproduire des processus sur la base d'un ensemble totalement non-ordonné d'évènements. Dans notre travail, nous soulevons les problèmes des contraintes de temps et de leurs paramétrages. Les méthodes proposées sont illustrées par des études de cas. La troisième partie du travail traite de la problématique des boucles inobservables qui peuvent résulter de comportements cycliques inobservables des systèmes considérés. Ce type de comportement conduit à un nombre infini d'événements dans les dépliages avec contraintes. La quatrième et dernière partie du travail est consacrée à l'implémentation des méthodes décrites précédemment. / This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.

Cette thèse s'intéresse à la modélisation et à l'analyse dessystèmes temps-réel distribués.Un système distribué est constitué de plusieurs composantsqui évoluent de manière partiellement indépendante. Lorsque des actionsexécutables par différentscomposants sont indépendantes, elles sont dites concurrentes.Dans ce cas, elles peuvent être exécutées dans n'importe quel ordre, sanss'influencer, et l'état atteint après ces actions ne dépend pas de leur ordred'exécution.Dans les systèmes temps-réel distribués, les contraintes de temps créent desdépendances complexes entre les composants et les événements qui ont lieu surces composants. Malgré l'omniprésence et l'aspect critique de ces systèmes,beaucoup de leurs propriétés restent encore à étudier.En particulier, la nature distribuée de ces systèmes est souvent laissée de côté.Notre travail s'appuie sur deux formalismesde modélisation: les réseaux de Petri temporels et les réseaux d'automatestemporisés, et est divisé en deux parties.Dans la première partie, nous mettons en évidence les différences entre lessystèmes temporisés centralisés et les systèmes temporisés distribués. Nouscomparons les formalismes principaux et leurs extensions, avec une approcheoriginale qui considère la concurrence.En particulier, nous montrons comment transformer un réseau de Petri temporelen un réseau d'automates temporisés qui a le même comportement distribué.Nous nous intéressons ensuite aux horloges partagées dans lesréseaux d'automates temporisés. Les horloges partagées sont problématiqueslorsque l'on envisage d'implanter ces modèles sur des architecturesdistribuées. Nous montrons comment se passer des horloges partagées, touten préservant le comportement distribué, lorsque cela est possible.Dans la seconde partie, nous nous attachons à formaliser les dépendancesentre les événements dans les représentations en ordre partieldes exécutions des réseaux de Petri (temporels ou non).Les réseaux d'occurrence sont une de ces représentations, et leur structuredonne directement les relations de causalité, conflit et concurrence entreles événements. Cependant, nous montrons que, même dans le cas non temporisé,certaines relations logiques entre les événements nepeuvent pas être directement décrites par ces relations structurelles.Après avoir formalisé les relations logiques en question, nous résolvons leproblème de synthèse suivant: étant donnée une formule logique qui décrit unensemble d'exécutions, construire un réseau d'occurrence associé,quand celui-ci existe.Nous étudions ensuite les relations logiques dans un cadre temporisé simplifié,et montrons que le temps crée des dépendances complexes entre les événements.Ces dépendances peuvent être utilisées pour définir des dépliages canoniques deréseaux de Petri temporels, dans ce cadre simplifié. / This thesis is concerned with the modeling and the analysis of distributedreal-time systems. In distributed systems, components evolve partlyindependently: concurrent actions may be performed in any order, withoutinfluencing each other and the state reached after these actions does notdepends on the order of execution. The time constraints in distributed real-timesystems create complex dependencies between the components and the events thatoccur. So far, distributed real-time systems have not been deeply studied, andin particular the distributed aspect of these systems is often left aside. Thisthesis explores distributed real-time systems. Our work on distributed real-timesystems is based on two formalisms: time Petri nets and networks of timedautomata, and is divided into two parts.In the first part, we highlight the differences between centralized anddistributed timed systems. We compare the main formalisms and their extensions,with a novel approach that focuses on the preservation of concurrency. Inparticular, we show how to translate a time Petri net into a network of timedautomata with the same distributed behavior. We then study a concurrency relatedproblem: shared clocks in networks of timed automata can be problematic when oneconsiders the implementation of a model on a multi-core architecture. We showhow to avoid shared clocks while preserving the distributed behavior, when thisis possible.In the second part, we focus on formalizing the dependencies between events inpartial order representations of the executions of Petri nets and time Petrinets. Occurrence nets is one of these partial order representations, and theirstructure directly provides the causality, conflict and concurrency relationsbetween events. However, we show that, even in the untimed case, some logicaldependencies between event occurrences are not directly described by thesestructural relations. After having formalized these logical dependencies, wesolve the following synthesis problem: from a formula that describes a set ofruns, we build an associated occurrence net. Then we study the logicalrelations in a simplified timed setting and show that time creates complexdependencies between event occurrences. These dependencies can be used to definea canonical unfolding, for this particular timed setting.