L'avancée technologique que les systèmes embarqués ont connue lors de ces dernières années les rend de plus en plus complexes. Ils sont non seulement responsables de la commande des différents composants mais aussi de leur surveillance. A l'occurrence d'événement pouvant mettre en danger la vie des utilisateurs, une certaine configuration du système est exécutée afin de maintenir le système dans un état dégradé mais sûr. Il est possible que la configuration échoue conduisant le système dans un état appelé " état redouté " avec des conséquences dramatiques pour le système et l'utilisateur. La description des scénarios qui mènent le système vers l'état redouté à partir d'un état de fonctionnement 'normal' permet de comprendre les raisons de la dérive afin de prévoir les configurations nécessaires qui permettent de les éviter Dans notre approche d'analyse de sûreté de fonctionnement des systèmes dynamiques, les scénarios sont générés à partir d'un modèle réseau de Petri. En s'appuyant sur la logique linéaire comme nouvelle représentation (basée sur les causalités) du modèle réseau de Petri, une analyse qualitative permet de déterminer un ordre partiel de franchissement des transitions et ainsi extraire les scénarios redoutés. La démarche est focalisée sur les parties du modèle intéressantes pour l'analyse de fiabilité évitant ainsi l'exploration de toutes les parties du système et le problème de l'explosion combinatoire. L'objectif final consiste en la détermination de scénarios minimaux. En effet, un scénario peut bien mener vers l'état redouté sans qu'il soit minimal. Il contient des événements qui ne sont pas strictement nécessaires à l'obtention finale de l'état critique redouté. De même que la notion de coupe minimale a été définie dans le cadre des arbres de défaillance, nous proposons une définition de ce qu'est un scénario minimal dans le cas des réseaux de Petri. Pour prendre en compte La nature hybride des systèmes, nous avons développé un simulateur hybride basé sur le couplage de l'algorithme de génération de scénarios redoutés avec un solveur d'équations différentielles. L'algorithme se charge de la partie discrète modélisée par le réseau de Petri et le solveur d'équations de la partie continue modélisée par un ensemble d'équations différentielles. Afin d'avoir une approche système pour l'analyse de la sûreté de fonctionnement, nous proposons une approche qui permet de prendre en compte les exigences de sûreté dans le processus d'ingénierie des exigences qui permet d'établir un modèle de traçabilité afin de s'assurer de la prise en compte de ces exigences tout au long du cycle de vie du système. L'approche est basée sur une norme de l'ingénierie système, en l'occurrence l'EIA-632.

Les travaux exposés dans ce mémoire portent sur la conception de l'architecture de conduite des systèmes automatisés de production. Ils ont été développés au sein du Laboratoire Universitaire de Recherche en Production Automatisée (LURPA - EA 1385). Il s'agit de travaux prospectifs dont l'objectif est de construire un cadre méthodologique formel de conception et d'évaluation d'architectures.<br /><br />La première partie est consacrée à l'exposé du cadre méthodologique retenu et comporte quatre chapitres dans lesquels sont successivement abordés :<br /><br /> * la problématique générale de la conception d'architectures de conduite, ainsi qu'une revue des \travaux scientifiques dans le domaine,<br /> * la présentation générale de la méthode proposée avec le point de vue des activités de conception, d'évaluation et de choix d'architecture,<br /> * la présentation détaillée de la construction d'architecture avec cette fois le point de vue des différents modèles produits,<br /> * la présentation détaillée d'évaluation et de choix de l'architecture retenue avec encore une fois le point de vue des modèles d'évaluation. <br /><br />La seconde partie du mémoire est destinée à préciser et à valider par l'exemple la méthode proposée. Pour ce faire, nous l'avons appliquée à la conception de l'architecture de conduite d'un poste de lance ment d'un transfert libre. Le plan de cette étude suit de manière ordonnée la démarche que nous avons présenté dans la première partie.

Nos travaux de recherche sont dédiés µa la mise en oeuvre d'une maintenance<br />centralisée dans les systèmes manufacturiers. A partir de l'état de l'art sur le service<br />maintenance dans les différentes industries, notre problèmatique s'est portée sur la mise<br />en place d'un système de maintenance dans une entreprise possédant plusieurs unités<br />de production et dont la réparation des parties défaillantes des machines requiert des<br />ressources bien adaptées aux diverses machines complexes.<br />Dans le contexte d'une maintenance centralisée, une démarche de conception d'un atelier<br />de maintenance est proposée. A partir d'une étude fonctionnelle des machines de produc-<br />tion, la structure de l'atelier est établie et les ressources sont déterminées qualitativement.<br />Ensuite, nous proposons un dimensionnement de l'atelier de maintenance, passant par<br />l'évaluation des performances et en intégrant les coûts de maintenance. Enfin, pour que<br />l'atelier de maintenance soit efficace aussi bien sur le plan technique qu'économique de<br />l'entreprise, des stratégies de maintenance sont déterminées pour chaque machine.

Cette thèse porte sur la vérification formelle de systèmes temps réel et procède par transformation de modèle entre l'algèbre de processus temporisée RT-LOTOS et les réseaux de Petri temporels étendus par des chronomètres et des données. Des schémas de traduction de RT-LOTOS vers ces réseaux de Petri étendus sont proposés et formellement prouvés. L'approche transformationnelle développée pour la partie " contrôle " de RT-LOTOS est étendue à la partie " données ". Le langage RT-LOTOS est lui même enrichi d'un opérateur de suspension reprise qui permet de modéliser et vérifier une classe plus large de systèmes temps réel Plusieurs études de cas attestent de l'efficacité des schémas de traduction proposés par rapport à des outils LOTOS ou RT-LOTOS développés antérieurement. L'approche proposée s'avère transposable à d'autres langages de modélisation en particulier le profil UML temps réel TURTLE (Timed UML and RT-LOTOS Environment).

Ce mémoire présente des travaux concernant la spécification, la modélisation et l'analyse de systèmes de contrôle-commande temps réel répartis sur un réseau de terrain. La problématique de modélisation de tels systèmes, qui doivent satisfaire des contraintes temporelles, réside dans la maîtrise de la taille et de la complexité des modèles. Pour cela, une méthodologie de modélisation est proposée ; elle repose sur les concepts de structuration, de modélisation et de validation modulaires au moyen du modèle formel Réseaux de Petri Temporisés Stochastiques. La structuration consiste en une décomposition hiérarchisée en blocs fonctionnels élémentaires. Une structure est proposée pour des entités de communication d'un réseau local temps réel, ainsi que pour un système temps réel de commande et surveillance réparties. La modélisation repose sur la construction et la composition de modèles de modules élémentaires. Les principes énoncés concernent la définition de règles de composition. Des modèles d'assertions logiques sont également proposés pour faciliter le passage des descriptions de comportements exprimées en langage naturel, à une modélisation en Réseaux de Petri Temporisés Stochastiques. La validation repose sur des étapes de composition partielle qui utilisent la modularité pour effectuer des vérifications ascendantes du comportement. Cette méthodologie est appliquée au réseau de terrain FIP, ainsi qu'au futur système de contrôle-commande de poste de transformation d'énergie électrique d'EDF. L'étude du réseau FIP porte plus particulièrement sur les services et mécanismes périodiques de couche application pour les échanges temps réel. Les analyses (qualitatives et quantitatives) effectuées sur l'application de EDF répartie sur le réseau FIP portent sur la vérification des propriétés fonctionnelles et des contraintes temporelles du système.

Cette thèse s'inscrit dans le cadre général de l'utilisation des techniques formelles lors de la phase conceptuelle des systèmes distribués temps-réel, et concerne plus précisément l'extension des pouvoirs d'expression et d'analyse du modèle Réseaux de Petri Temporisés Stochastiques. Ce modèle, qui appartient à la classe des Réseaux de Petri Stochastiques, associe à chaque transition un intervalle de temps, et une distribution de probabilité sur cet intervalle (ceci permet de représenter des caractéristiques temporelles variées et en particulier des contraintes) En ce qui concerne le pouvoir d'expression, nous avons introduit, d'une part, la notion de mémoire temporelle de toutes les sensibilisations (ceci est important pour l'étude des phénomènes de préemption que l'on rencontre dans des algorithmes d'ordonnancement et dans des problèmes de sûreté de fonctionnement) et, d'autre part, plusieurs règles de tir de transitions (en particulier les règles MIN et MAX qui permettent des études des cas pires, aspect important dans les systèmes temps-réels). Les graphes ainsi obtenus ont été également situés par rapport à la référence comportementale que constitue le graphe des classes d'états (obtenu à partir des Réseaux de Petri Temporels). En ce qui concerne le pouvoir d'analyse, nous avons défini le concept d'automate quotient quantifié (concept basé, à la fois, sur la relation d'équivalence de Milner et les règles de réduction de Beizer), qui a deux qualités importantes : il permet, d'une part, d'obtenir des modèles, à la fois qualitatifs et quantitatifs de services de communication ; et, d'autre part, de contrôler les dimensions des modèles à traiter lors de la modélisation d'architectures de communication multicouches. Ce modèle a été appliqué à un exemple industriel, le protocole embarqué temps-réel ARINC 629 CP. L'étude faite a mis en évidence les propriétés temps-réel et de tolérance aux pannes de ce protocole.

Cette thèse traite de la modélisation des systèmes temps-réel à l'aide<br />de réseaux de Petri. Nous considérons séparément la question de<br />représentation du temps et celle de la préemption (interruption des<br />processus d'un système) qui est d'un usage courant pour les<br />applications temps-réel.<br /><br />Nous utilisons des réseaux de Petri sans extension par des<br />informations concernant le temps. Notre approche consiste alors à<br />introduire le temps par des sous-réseaux spécifiques représentant les<br />horloges du système modélisé. Le résultat est appelé temps<br />causal puisque seule la causalité définit la relation de précédence<br />entre les occurrences des événements. Afin d'obtenir une formulation<br />élégante de l'approche causale du temps, nous utilisons le modèle des<br />M-nets, une classe de réseaux de Petri colorés composables à la<br />manière des algèbres de processus. Nous étendons ce modèle de façon à<br />permettre la représentation efficace des communications asynchrones<br />entre processus et les bases théoriques liées à cette extension sont<br />revisitées et mises à jour. Nous utilisons les M-nets ainsi étendus<br />pour modéliser plusieurs horloges aux fonctionnalités différentes.<br />Nous montrons comment des systèmes à plusieurs horloges, synchronisées<br />ou non, peuvent être assez simplement obtenus. La pertinence de notre<br />approche est évaluée par une étude de cas et appliquée à la sémantique<br />d'une extension d'un langage de programmation parallèle, appelé<br />B(PN)², par des instructions liées au temps.<br /><br />Pour introduire la préemption nous proposons une nouvelle extension<br />des M-nets avec des opérations permettant la suspension/reprise et<br />l'avortement. Le modèle obtenu est étudié sur le plan théorique et<br />appliqué à l'extension de la sémantique de B(PN)² par des exceptions<br />et un système de tâches.

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

Cette thèse s'attaque dans une première partie au problème du pilotage automatique des voiliers de compétition en s'appuyant sur la réalité virtuelle qui, via la simulation, permet de s'affranchir de tests en situation réelle généralement coûteux, contraignants et risqués. Une architecture multi-agents est proposée ainsi que sa modélisation en termes de réseaux de Petri. Une deuxième partie est consacrée à la présentation et à l'étude de plusieurs extensions algébriques de ces réseaux dans le but initial de prendre en charge certaines caractéristiques des systèmes à évènements discrets non couvertes par les réseaux places/transitions usuels. Un état de l'art présente différentes approches du problème du pilotage des voiliers et souligne son caractère complexe. Partant du constat que malgré tout, l'homme parvient généralement à faire face à la plupart des situations rencontrées en mer, nous proposons d'asseoir notre système sur une expertise très fine de la pratique du barreur de compétition. Cette dernière permet d'identifier et de caractériser les éléments importants liés à la technique de barre. Nous proposons ensuite une architecture multi-agents dont la partie commande est basée sur trois agents autonomes, asynchrones et concurrents ainsi que sa modélisation par réseaux de Petri synchronisés. Le système est implémenté sous ARéVi, moteur de simulation d'objets actifs et de rendu 3D développé au CERV. L'expérimentation montre que le barreur virtuel ainsi créé assure un niveau de sécurité intéressant pour un coureur au large en réagissant aux sollicitations de son voilier d'une manière proche de celle d'un homme. Le gain en performance semble plus limité du fait, en particulier, des faiblesses du modèle de bateau implémenté mais pourrait s'avérer intéressant sur un voilier réel. Dans la deuxième partie de cette thèse nous proposons différentes extensions algébriques des réseaux de Petri. Nous choisissons tout d'abord d'utiliser un groupe à la place de l'algèbre des places usuelle des réseaux de Petri et d'en priver l'accès à l'élément neutre pour interdire certaines transitions. Ces réseaux, appelés strict-group-nets, étendent en particulier les réseaux de Petri purs si on choisit pour groupe l'ensemble des entiers relatifs. L'adjonction d'arcs dits inconditionnels conduit aux group-nets et permet d'englober également les réseaux impurs. Nous montrons que les problèmes de savoir si les Z-nets et les strict-Z-nets sont bornés et si une place de ces réseaux est bornée sont décidables via la définition d'un arbre proche de celle d'un arbre de couverture. La notion de ressource disparaissant dans ces nouveaux réseaux, plutôt que de choisir une algèbre a priori nous cherchons à caractériser les algèbres permettant de singer le comportement des réseaux de Petri usuels. Cette démarche conduit aux réseaux lexicographiques pour lesquels la notion de ressource reste étrange car on peut consommer indéfiniment strictement. Nous montrons que les réseaux lexicographiques ont la puissance des machines de Turing et que les réseaux lexicographiques bornés sont les réseaux de Petri bornés. Nous démontrons enfin que le problème de la synthèse trouve une réponse polynomiale pour les Z/2Z-nets ainsi que pour les réseaux lexicographiques en termes de meilleure approximation d'un langage régulier donné.

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