Les systèmes d'information actuels doivent, à la fois, protéger les informations qui leur sont confiées et se plier à des environnements opérationnels variables. Cesdeux objectifs, sécurité et flexibilité, peuvent être antinomiques. Ce conflit conduit généralement à l'utilisation de systèmes offrant un niveau de sécurité acceptable, mais non maximal. Définir un tel niveau présuppose l'existence de méthodes d'évaluation de la sécurité. Cette problématique fait l'objet de cette thèse. L'auteur y passe en revue les différents critères d'évaluation existant ainsi que les méthodes dites d'analyse de risques. Ceci introduit la nécessité de définir un cadre formel capable de modéliser tout système et d'évaluer dans quelle mesure il satisfait à des objectifs de protection précis.<br />Les modèles formels développés pour l'étude de la sécurité informatique, n'offrent pas le cadre mathématique désiré. L'auteur montre qu'ils adoptent une hypothèse de pire cas sur le comportement des utilisateurs, incompatible avec une modélisation réaliste. Après avoir montré, sur la base du modèle take-grant, comment s'affranchir de cette hypothèse, l'auteur définit un nouveau modèle, le graphe des privilèges, plus efficace pour gérer certains problèmes de protection. Il illustre son utilisation dans le cadre des systèmes Unix.<br />Enfin, l'auteur propose d'évaluer la sécurité en calculant le temps et l'effort nécessaires à un intrus pour violer les objectifs de protection. Il montre comment définir un cadre mathématique apte à représenter le système pour obtenir de telles mesures. Pour cela, le graphe des privilèges est transformé en un réseau de Petri stochastique et son graphe des marquages est dérivé. Les mesures sont calculées sur cette dernière structure et leurs propriétés mathématiques sont démontrées. L'auteur illustre l'utilité du modèle par quelques résultats issus d'un prototype développé afin d'étudier la sécurité opérationnelle d'un système Unix.

Dans le transport ferroviaire, le coût et la disponibilité du matériel roulant sont des questions majeures. Pour optimiser le coût de maintenance du système de transport ferroviaire, une solution consiste à mieux détecter et diagnostiquer les défaillances. Actuellement, les architectures de surveillance/diagnostic centralisées atteignent leurs limites et imposent d'innover. Cette innovation technologique peut se matérialiser par la mise en oeuvre d'architectures embarquées de surveillance/diagnostic distribuées et communicantes afin de détecter et localiser plus rapidement les défaillances et de les valider dans le contexte opérationnel du train. Les présents travaux de doctorat, menés dans le cadre du FUI SURFER (SURveillance active Ferroviaire) coordonné par Bombardier, visent à proposer une démarche méthodologique d'évaluation de la sûreté de fonctionnement d'architectures de surveillance/diagnostic. Pour ce faire, une caractérisation et une modélisation génériques des architectures de surveillance/diagnostic basée sur le formalisme des Réseaux de Petri stochastiques ont été proposées. Ces modèles génériques intègrent les réseaux de communication (et les modes de défaillances associés) qui constituent un point dur des architectures de surveillance/diagnostic retenues. Les modèles proposés ont été implantés et validés théoriquement par simulation et une étude de sensibilité de ces architectures de surveillance/diagnostic à certains paramètres influents a été menée. Enfin, ces modèles génériques sont appliqués sur un cas réel du domaine ferroviaire, les systèmes accès voyageurs des trains, qui sont critiques en matière de disponibilité et diagnosticabilité.

Cette thèse a été réalisée dans le cadre du projet « Gestion et Optimisation de la Chaîne Documentaire », projet labellisé par le Pôle de compétitivité des Industries du Commerce. Le projet a pour but de concevoir et de développer un nouveau workflow et un outil d’aide à la décision. Ce système doit être capable de gérer et d’optimiser le flux complet dématérialisé de contrats reçus à COFIDIS.Nous présentons d’abord le framework retenu dans le cadre du projet pour modéliser et implémenter le workflow. En phase de conception BPMN a été choisi. Pour la partie développement, l’utilisation de BPEL a été préconisée pour implémenter et exécuter l'application finale (services web).Cependant la flexibilité offerte par BPMN peut conduire à des propriétés indésirables du processus telles que blocage et inaccessibilité. De plus, BPMN a été conçu pour fournir des modèles Orientés Process. Les données ou les ressources y sont donc peu représentées. En conséquence, l'analyse de performance sur un modèle BPMN est quasi inexistante.Afin de surmonter ces problèmes nous proposons d’insérer dans le framework deux nouvelles phases. Ces deux phases sont appliquées au modèle BPMN. La première est une phase de vérification et de validation et la deuxième une phase d'optimisation. Ces deux phases sont réalisées en transformant le modèle BPMN vers un langage formel. Notre choix dans ce travail a été d'utiliser les réseaux de Petri. Ce qui nous a permis de vérifier et de valider de bonnes propriétés du process. Quant à l’optimisation, nous avons défini une nouvelle variante du problème d’affectation (bin packing problem) et proposé une résolution à intégrer dans le processus d’aide à la décision / This thesis has been realized as a part of the project GOCD (French acronym for Management and optimization of document life cycle) and within the context of the French competitive cluster PICOM. The project aims to design and develop a new paperless workflow system and decision making tool to replace the current paper based system. The new workflow system must manage and optimize received credit demands at COFIDIS.The first part of this thesis presents and discusses a framework to model and implement workflow systems. The proposed framework allows more flexibility in workflow reengineering process and operational analysis for different business process. The proposed framework uses the most recent and promising language to model and execute workflow the Business Process Modeling Notation (BPMN) and Business Process Execution Language (BPEL).The flexibility offered by BPMN can also lead to undesirable properties for business process such as deadlocks and unreachablity. More, BPMN notation was designed to model business process, and little consideration was concentrated to represent data and resources. As a result, carrying out performance analysis on a BPMN model is also limited.To overcome these problems, we propose two additional phases in the reengineering process. They are applied to the target BPMN model. The first phase is verification and validation and the second one is optimization. These two phases are realized by transforming the BPMN model to a formal language, Petri nets. As for optimization, a new variant of bin packing problem has been defined. And we propose to integrate its resolution in a decision making tool

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

Les services de stérilisation sont des lieux de production de soins caractérisés par une multitude d’activités et situations auxquelles ils sont confrontés. En outre, les services de stérilisation doivent assurer leurs missions dans un environnement caractérisé par la présence d’une variété de risques. Les risques présents dans ces milieux peuvent aller des pannes des équipements jusqu’aux contaminations et transmission des maladies nosocomiales. Ces services sont aussi tenus de garder un niveau de performances satisfaisant pour assurer la continuité des soins dans les blocs opératoires.Pour aider ces services dans leur quête d'un système performant, capable d’évoluer dans un environnement à haut niveau de risques, nous nous intéressons dans ce travail de recherche au développement d’une approche intégrée pour l’analyse de risques et l’évaluation des performances. Ce travail s’intègre dans un cadre collaboratif entre le laboratoire G-SCOP et le service de stérilisation du CHU de Grenoble, terrain d’étude choisi pour mettre en œuvre l’approche proposée.L'approche que nous proposons se déroule en plusieurs étapes: tout d’abord, suite à une comparaison entre les méthodes de gestion des risques, nous nous sommes orientés vers l’approche pilotée par modèle, dénommée FIS (Fonction Interaction Structure). En nous basant sur FIS, nous avons développé un modèle de risque dans ce service de stérilisation, décrivant à la fois les fonctions, les ressources permettant la réalisation de ces fonctions ainsi que les différents risques qui peuvent être rencontrés. Dans un deuxième temps, nous avons représenté le comportement dynamique du modèle de risques obtenu. Ce modèle dynamique permet de simuler le comportement du service de stérilisation et le voir évoluer dans les situations normales de fonctionnement et les situations de risques. Pour ce faire, nous avons introduit une nouvelle classe de réseau de Petri appelée réseau de Petri PTPS (Predicate-Transition, Prioritized, Synchronous) permettant de représenter et simuler le comportement dynamique du modèle FIS. Par la suite, nous avons automatisé le passage entre le modèle de risque et le modèle dynamique. Cette automatisation est effectuée par un ensemble d’algorithmes de traduction, capables de convertir automatiquement le modèle FIS et le modèle de simulation en réseau de Petri PTPS.Cette approche a donné lieu à un outil de modélisation et de simulation en mode dégradé, appelé SIM-RISK. Nous avons également montré l’utilité de cet outil sur des exemples inspirés des différents risques rencontrés dans le service de stérilisation. / Sterilization services are vulnerable to risks, due to the contagious nature of their environment and to the degradation that risks can cause to their performances and to the safety of patients and staff. The risks in these facilities can range from equipment failure to the transmission of nosocomial infections and diseases. In this kind of high risk environment, these services are also required to maintain an adequate level of performance to ensure continuity of care in operating theaters.We focus in this research on the development of an integrated approach for risk analysis and performance assessment. This work is part of a collaborative work between the G-SCOP laboratory and the sterilization service of the University Hospital of Grenoble, which was the case study chosen to implement the proposed approach.The approach we propose is conducted in several steps: first, following a comparison of the risk analysis methods, we have chosen a model driven approach called FIS (Function Interaction Structure). Based on FIS, we have developed a risk model of Grenoble University Hospital sterilization service. This model describes the functions, the resources to achieve these functions as well as the various risks that may be encountered. Secondly, we introduced a new view to the FIS model dedicated to describe the dynamic behaviour of the resulting risk model.This dynamic model can simulate the behaviour of the sterilization service in normal situations of operations and risk situations.To do this, we have introduced a new Petri Net class called PTPS (Predicate-Transition, Prioritized, Synchronous) Petri Net to represent and simulate the dynamic behaviour of the FIS model. Subsequently, we automated the switching between the risk model and the dynamic model. This automation is performed by a set of translation algorithms capable of automatically converting the FIS model to a PTPS Petri Net simulation model .This approach resulted in a modelling and simulation tool in degraded mode called SIM-RISK. We also showed the usefulness of this tool by some examples based on different risks encountered in the sterilization service.

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. / The place-invariants method is one of the most popular controller synthesis approaches for Petri net (PN) modeled DES. Unfortunately, the observance of the constraints is not certain in the presence of uncontrollable transitions. This thesis offers a solution to this problem for ordinary and generalized PNs. We begin by studying safe non-conservative PNs, and devising a constraint-determination technique that will always provide a set of admissible constraints for this type of model. The approach stems from the general definition of forbidden states --- that of marking vectors. In the second part of our work, we present an admissible constraint-determination technique for generalized PNs. The method is based on a special view of the system's state space. The constraints are derived from the equation of the affine hyper-plane separating the authorized- and forbidden- regions of this space. We propose an algorithm that allows the identification of the minimal maximally permissive controller.

Afin de faire face à différents types de stress et s'adapter à de nouveaux environnements, les bactéries ont développé de nombreux mécanismes génétiquement régulés. La compétence pour la transformation naturelle est un processus qui favorise le transfert horizontal de gènes. Si les espèces phylogénétiquement éloignées partagent des mécanismes conservés d'intégration et de remaniement de l'ADN, les circuits de régulation de la compétence ne sont toutefois pas universels mais adaptés au mode de vie de chaque espèce. Chez les bactéries Gram-positives, les cascades de régulation de Streptococcus pneumoniae et Bacillus subtilis sont les mieux documentées. Si de nombreux modèles mathématiques ont été établis pour étudier différents aspects de la régulation des compétences chez B. subtilis, un seul modèle à échelle de population a été développé pour S. pneumoniae, il y a plus de dix ans, sur la base d'hypothèses contestées par de nouvelles données expérimentales. Nous avons développé, chez S. pneumoniae, un modèle fondé sur la connaissance de la régulation de la compétence qui intègre les éléments biologiques essentiels connus à ce jour. La cohérence structurelle de la topologie du réseau est confirmée par le formalisme des réseaux de Petri. Le réseau est ensuite transformé en un ensemble d'équations différentielles ordinaires pour étudier son comportement dynamique. La cinétique des protéines a été estimée en utilisant des données de luminescence et l'estimation des paramètres a été contrainte à partir des connaissances disponibles. Après avoir testé des modèles alternatifs, nous avons proposé l'existence d'un produit de gène tardif supplémentaire pouvant inhiber l'action de ComW, l'activateur du facteur sx. Nous apportons également un nouvel éclairage sur cette cascade de régulation en prédisant la cinétique de composantes du système qui pourraient être impliquées dans des comportements spécifiques. Ce modèle consolide les connaissances expérimentales acquises sur la régulation de la compétence chez S. pneumoniae. De plus, il peut être appliqué aux autres espèces de streptocoques appartenant aux groupes mitis et anginosus puisqu'ils partagent le même circuit régulateur. À l'échelle populationnelle, la transition vers l'état de compétence se produit d'abord dans une sous-population de cellules et se propage ensuite dans toute la population par contact physique cellule à cellule. En permettant la simulation du comportement d'une cellule individuelle, le modèle pourra servir de module dans la conception d'un modèle d'une population bactérienne composée de cellules hétérogènes. / Bacteria have evolved many types of genetically induced mechanisms to face different types of stresses and to adapt to new environments. Competence for natural transformation is one such process that promotes horizontal gene transfer. If phylogenetically distant species share conserved uptake and processing apparatus, competence regulatory circuits are not universal but adapted to every species' lifestyle. In Gram-positive bacteria, Streptococcus pneumoniae and Bacillus subtilis regulatory cascades are the best documented. If many mathematical models have been established to study different aspects of competence regulation in B. subtilis, only one population-scaled model has been developed for S. pneumoniae, a decade ago, based on hypotheses that are challenged by new experimental data. We develop, in S. pneumoniae, a knowledge-based model of the competence regulation at cell level that integrates the enriched biological knowledge acquired to date. The structural consistency of the network topology is confirmed using Petri net formalism. The network is further turned into a set of ordinary differential equations to study its dynamics behavior. Protein kinetics are estimated using time-series luminescence data and other parameter estimations are constrained according to available knowledge. We point out some gap in competence shut-off knowledge, and, after testing alternative models, we predict the requirement of a yet unknown late com gene product inhibiting the action of ComW, the ?x factor activator. We also bring new insights into this regulatory cascade by predicting the system components that might be involved in specific experimental behavior. Our model consolidates the experimental knowledge acquired on competence regulation in S. pneumoniae. Moreover, it can be applied to the other streptococci species belonging to the mitis and anginosus groups since they shared the same regulatory circuit. In the population, the competence shift happens first in a subpopulation of cells and spreads into the whole population through cell to cell contact. Allowing simulation of individual cell behavior, our model will provide a brick for the design of a population-scale model composed of heterogeneous cells.

Le développement et l’application des langages formels sont un défi à long terme pour la science informatique. Un enjeu particulier est l’acceptation par l’industrie. Cette thèse présente une approche pour la modélisation et la vérification des postes d’aiguillage français. La première question est la modélisation du système d’enclenchement par les réseaux de Petri colorés (RdPC). Un cadre de modélisation générique et compact est introduit, dans lequel les règles d’enclenchement sont modélisées dans une structure hiérarchique, tandis que les installations sont modélisées dans une perspective géographique. Ensuite, un patron de modèle est présenté. C’est un modèle paramétré qui intègre les règles nationales françaises qui peut être appliquée pour différentes gares. Puis, un concept basé sur l’événement est présenté dans le processus de modélisation des parties basses des postes d’aiguillage. La deuxième question est la transformation des RdPCs en machines B, qui va aider les concepteurs sur la route de l’analyse à application. Tout d’abord, une méthodologie détaillée, s’appuyant sur une table de correspondance, du RdPCs non-hiérarchiques vers les notations B est présentée. Ensuite, la hiérarchie et la priorité des transitions du RdPC sont successivement intégrées dans le processus de mapping, afin d’enrichir les possibilités de types de modèles en entrées de la transformation. Les machines B produites par la transformation permettent la preuve automatique intégrale par l’Atelier B. L’ensemble de ces travaux, chacun à leur niveau, contribuent à renforcer l’efficacité d’un cadre global d’analyse sécuritaire / Development and application of formal languages are a long-standing challenge within the computer science domain. One particular challenge is the acceptance of industry. This thesis presents some model-based methodologies for modelling and verification of the French railway interlocking systems (RIS). The first issue is the modellization of interlocking system by coloured Petri nets (CPNs). A generic and compact modelling framework is introduced, in which the interlocking rules are modelled in a hierarchical structure while the railway layout is modelled in a geographical perspective. Then, a modelling pattern is presented, which is a parameterized model respecting the French national rules. It is a reusable solution that can be applied in different stations. Then, an event-based concept is brought into the modelling process of low-level part of RIS to better describe internal interactions of relay-based logic. The second issue is the transformation of coloured Petri nets into B machines, which can help designers on the way from analysis to implementation. Firstly, a detailed mapping methodology from non-hierarchical CPNs to abstract B machine notations is presented. Then the hierarchy and the transition priority of CPNs are successively integrated into the mapping process, in order to enrich the adaptability of the transformation. This transformation is compatible with various types of colour sets and the transformed B machines can be automatically proved by Atelier B. All these works at different levels contribute towards a global safe analysis framework

Un environnement spatial naturel hostile, les systèmes spatiaux de télédétection traditionnels,monolithiques et téléopérés depuis le sol, demeurent vulnérables face à un nombre croissant de menaces émergentes issues de l’environnement spatial artificiel (armes antisatellites,débris). Plutôt que de chercher à protéger physiquement les satellites, nous proposons d’adopter une stratégie fondée sur le concept de résilience, qui traduit la capacité d’un système à poursuivre sa mission face à des aléas imprévisibles, fût-ce en mode dégradé. En nous appuyant sur de récentes innovations dans les technologies spatiales, nous nous sommes intéressés à la conception et à l’évaluation d’architectures système fondées sur la mise en réseau de constellations de microsatellites hétérogènes, autonomes et communicants.Afin d’étudier de telles architectures, appelées réseaux de constellations autonomes (RCA),nous proposons une approche de modélisation ainsi qu’un outil de simulation à base de réseaux de Petri imbriqués. Grâce à des métriques issues des réseaux de télécommunication ainsi que des systèmes multiagents, nous avons évalué les RCA au travers de leurs performances opérationnelles et de leurs capacités de communication, nominales puis dans divers modes dégradés. Du point de vue de la résilience, les résultats présentés mettent en évidence l’intérêt de disposer de réseaux de communication denses et de modules de reconfiguration autonomes embarqués au sein même des satellites. / Although Earth observation space systems are designed with strong safety requirements due to an hostile natural space environment, they remain vulnerable to an increasing range of emerging space threats such as antisatellite weapons or orbital debris. Instead of a physical protection of these monolithic and remote-controlled assets, we propose a design strategy based on the concept of resilience which is the ability of a system to maintain an acceptable level of performance in the presence of unforeseeable disturbance.Thanks to the latest space technology innovations, we devised new system architectures composed of networked constellations of heterogeneous and autonomous interacting microsatellites. We decided to model these architectures, called autonomous networked constellations (RCA in French), thanks to Petri nets, and more specifically their nets-within-nets variant. Using telecommunication and multiagent metrics, we assessed different RCA configurations through their operational performance and communicability, for nominal as wellas degraded modes. From the resilience point of view, we present quantitative results that point out the benefits of dense space networks and embedded autonomous reconfiguration modules.

Les travaux de cette thèse portent sur l'analyse des comportements chaotiques dans les convertisseurs multicellulaires séries. Ces systèmes à commutationpeuvent présenter une variété de phénomènes complexes liés à des bifurcationset au chaos. Sachant qu'un convertisseur de puissance qui a une charge purementdissipative, ne peut générer un comportement chaotique, nous avons dans la première partie de cette thèse, connecté un hacheur à deux cellules à une charge non linéaire non strictement dissipative et nous avons analysé ses comportements à l'aide des propriétés dynamiques de base et présenté les routes vers le chaos. La fin de cette partie a été consacrée à l'étude du hacheur à cinq cellules qui est une généralisation du hacheur à deux cellules. Afin de supprimer le comportement chaotique, la deuxième partie du travail a été consacrée à la synthèse d'une loi de commande hybride basé sur la modélisation par réseaux de Petri pour la régulation des tensions des condensateurs flottants et du courant de charge. / This thesis deals with the analysis of chaotic behaviors in serial multicellularconverters. These switching systems can have a variety of complex phenomenaassociated with bifurcations and chaos. Knowing that a power converter that has a purely dissipative load cannot generate chaotic behavior, we've in the first part of this thesis, we connected a two-cell chopper to a nonlinear load not strictly dissipative and we've analyzed its behaviors by using some basic dynamic properties and thus presented the routes to chaos. The end of this part was devoted to the study of the 5-cell chopper which is a generalization of the two-cell chopper. In order to eliminate the chaotic behavior, the second part was devoted to the synthesis of a controlled law based on hybrid modeling of Petri nets for the regulation of capacitor voltages and current load.