To see the other types of publications on this topic, follow the link: Sécurité des systèmes – Vérification de modèles (informatique).
Dissertations / Theses on the topic 'Sécurité des systèmes – Vérification de modèles (informatique)'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 50 dissertations / theses for your research on the topic 'Sécurité des systèmes – Vérification de modèles (informatique).'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.
1
Antakly, Dimitri. "Apprentissage et vérification statistique pour la sécurité." Thesis, Nantes, 2020. http://www.theses.fr/2020NANT4015.
Full textAbstract:
Les principaux objectifs poursuivis au cours de cette thèse sont en premier lieu de pouvoir combiner les avantages de l’apprentissage graphique probabiliste de modèles et de la vérification formelle afin de pouvoir construire une nouvelle stratégie pour les évaluations de sécurité. D’autre part, il s’agit d’évaluer la sécurité d’un système réel donné. Par conséquent, nous proposons une approche où un "Recursive Timescale Graphical Event Model (RTGEM)" appris d’après un flux d’évènements est considéré comme représentatif du système sous-jacent. Ce modèle est ensuite utilisé pour vérifier une propriété de sécurité. Si la propriété n’est pas vérifiée, nous proposons une méthodologie de recherche afin de trouver un autre modèle qui la vérifiera. Nous analysons et justifions les différentes techniques utilisées dans notre approche et nous adaptons une mesure de distance entre Graphical Event Models. La mesure de distance entre le modèle appris et le proximal secure model trouvé nous donne un aperçu d’à quel point notre système réel est loin de vérifier la propriété donnée. Dans un soucis d’exhaustivité, nous proposons des séries d’expériences sur des données de synthèse nous permettant de fournir des preuves expérimentales que nous pouvons atteindre les objectifs visésThe main objective of this thesis is to combine the advantages of probabilistic graphical model learning and formal verification in order to build a novel strategy for security assessments. The second objective is to assess the security of a given system by verifying whether it satisfies given properties and, if not, how far is it from satisfying them. We are interested in performing formal verification of this system based on event sequences collected from its execution. Consequently, we propose a model-based approach where a Recursive Timescale Graphical Event Model (RTGEM), learned from the event streams, is considered to be representative of the underlying system. This model is then used to check a security property. If the property is not verified, we propose a search methodology to find another close model that satisfies it. We discuss and justify the different techniques we use in our approach and we adapt a distance measure between Graphical Event Models. The distance measure between the learned "fittest" model and the found proximal secure model gives an insight on how far our real system is from verifying the given property. For the sake of completeness, we propose series of experiments on synthetic data allowing to provide experimental evidence that we can attain the desired goals
2
Bursuc, Sergiu. "Contraintes de déductibilité dans une algèbre quotient : réduction de modèles et applications à la sécurité." Cachan, Ecole normale supérieure, 2009. http://www.theses.fr/2009DENS0055.
Full textAbstract:
Dans cette thèse, nous nous intéressons à la vérification des protocoles de sécurité. Ce sont des programmes dont le but est d'établir une communication sûre entre plusieurs agents. Quasiment toutes les applications modernes ont besoin des protocoles de sécurité pour assurer leur bon fonctionnement, ce qui rend d'autant plus importante la question de leur correction et demande une réponse basée sur des arguments rigoureux. Les méthodes formelles, où les messages et les opérations sont abstraits par une algèbre de termes, se sont avérées cruciales dans cette démarche. Cependant, pour avoir une modélisation fidèle de la réalité, l'algèbrene peut être libre, mais doit incorporer des propriétés des algorithmes utilisées pour construire les messages. Dans ce contexte, motivés à la fois par des besoins pratiques et des intérêts théoriques, nous étudions les techniques générales pour la vérification des propriétés de sécurité de protocoles modulo une théorie équationnelle, à travers la résolution de contraintes de déductibilitéTo enable formal and automated analysis of security protocols, one has to abstract implementations of cryptographic primitives by terms in a given algebra. However, the algebra can not be free, as cryptographic primitives have algebraic properties that are either relevant to their specification or else they can be simply observed in implementations at hand. These properties are sometimes essential for the execution of the protocol, but they also open the possibility for an attack, as they give to an intruder the means to deduce new information from the messages that he intercepts over the network. In consequence, there was much work over the last few years towards enriching the Dolev-Yao model, originally based on a free algebra, with algebraic properties, modelled by equational theories. In this thesis, driven by both practical and theoretical interests, we propose general decision procedures for the insecurity of protocols, that can be applied to several classes of equational theories
3
Lugou, Florian. "Environnement pour l'analyse de sécurité d'objets communicants." Thesis, Université Côte d'Azur (ComUE), 2018. http://www.theses.fr/2018AZUR4005/document.
Full textAbstract:
Alors que les systèmes embarqués sont de plus en plus nombreux, complexes, connectés et chargés de tâches critiques, la question de comment intégrer l'analyse précise de sécurité à la conception de systèmes embarqués doit trouver une réponse. Dans cette thèse, nous étudions comment les méthodes de vérification formelle automatiques peuvent aider les concepteurs de systèmes embarqués à évaluer l'impact des modifications logicielles et matérielles sur la sécurité des systèmes. Une des spécificités des systèmes embarqués est qu'ils sont décrits sous la forme de composants logiciels et matériels interagissant. Vérifier formellement de tels systèmes demande de prendre tous ces composants en compte. Nous proposons un exemple d'un tel système (basé sur Intel SGX) qui permet d'établir un canal sécurisé entre un périphérique et une application. Il est possible d'en vérifier un modèle de haut-niveau ou une implémentation bas-niveau. Ces deux niveaux diffèrent dans le degré d'intrication entre matériel et logiciel. Dans le premier cas, nous proposons une approche orientée modèle, à la fois au niveau partitionnement et conception logicielle, permettant une description à haut niveau d'abstraction du matériel et du logiciel et permettant une transformation de ces modèles en une spécification formelle sur laquelle une analyse de sécurité peut être effectuée avec l'outil ProVerif. Dans le second cas, nous considérons une implémentation logicielle et un modèle matériel plus concret pour effectuer des analyses de sécurité plus précises toujours avec ProVerifAs embedded systems become more complex, more connected and more involved in critical tasks, the question of how strict security analysis can be performed during embedded system design needs to be thoroughly addressed. In this thesis, we study how automated formal verification can help embedded system designers in evaluating the impact of hardware and software modifications on the security of the whole system. One of the specificities of embedded system design-which is of particular interest for formal verification-is that the system under design is described as interacting hardware and software components. Formally verifying these systems requires taking both types of components into account. To illustrate this fact, we propose an example of a hardware/software co-design (based on Intel SGX) that provides a secure channel between a peripheral and an application. Formal verification can be performed on this system at different levels: from a high-level view (without describing the implementations) or from a low-level implementation. These two cases differ in terms of how tightly coupled the hardware and software components are. In the first case, we propose a model-based approach-for both the partitioning and software design phases- which enables us to describe software and hardware with high-level models and enables a transformation of these models into a formal specification which can be formally analyzed by the ProVerif tool. In the second case, we consider a software implementation and a more concrete
4
Robin, Ludovic. "Vérification formelle de protocoles basés sur de courtes chaines authentifiées." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0019/document.
Full textAbstract:
Les protocoles de sécurité modernes peuvent impliquer un participant humain de façon à ce qu'il compare ou copie de courtes chaines de caractères faisant le pont entre différents appareils. C'est par exemple le cas des protocoles basés sur une authentification à facteur multiples comme les protocoles Google 2 factor ou 3D-Secure.Cependant, de telles chaines de caractères peuvent être sujettes à des attaques par force brute. Dans cette thèse nous proposons un modèle symbolique qui inclut les capacités de l'attaquant à deviner des secrets faibles et à produire des collisions avec des fonctions de hachage dont de l'application résulte une courte chaine de caractères. Nous proposons une nouvelle procédure de décision pour analyser un protocole (restreint à un nombre borné de sessions) qui se base sur de courtes chaines de caractères. Cette procédure a été intégré dans l'outil AKISS et testé sur les protocoles du standard ISO/IEC 9798-6:2010Modern security protocols may involve humans in order to compare or copy short strings betweendifferent devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-Secure are typical examplesof such protocols. However, such short strings may be subject to brute force attacks. In this thesis we propose asymbolic model which includes attacker capabilities for both guessing short strings, and producing collisions whenshort strings result from an application of weak hash functions. We propose a new decision procedure for analyzing(a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in theAKISS tool and tested protocols from the ISO/IEC 9798-6:2010 standard
5
Sun, Tithnara Nicolas. "Modélisation et analyse formelle de modèles système pour les menaces persistantes avancées." Electronic Thesis or Diss., Brest, École nationale supérieure de techniques avancées Bretagne, 2022. http://www.theses.fr/2022ENTA0004.
Full textAbstract:
La criticité croissante des systèmes industriels les expose davantage aux menaces du monde cyber. En particulier les menaces persistantes avancées ou Advanced Persistent Threats (APT) sont des attaquants sophistiqués dotés de ressources conséquentes et ciblant spécifiquement les systèmes critiques. Les méthodologies de cyber-défense actuelles permettent de protéger les systèmes contre les cyber-menaces classiques mais elles peinent à contrer efficacement les APT. En effet, les APT usent de stratégies complexes et de tactiques de dissimulation qui les rendent difficile à contrecarrer. Pour répondre à ce besoin, la méthodologie d’Operational Design tirée des stratégies militaires permet de mieux comprendre l’établissement de stratégie de ces attaquants sophistiqués. Cette méthodologie axée sur la mission et adaptée au contexte des APT repose sur la fédération de plusieurs processus de spécification, de modélisation et d’analyse pour produire une stratégie opérationnelle. Pour évaluer cette approche, un outillage fédéré complet a été conçu et appliqué à un cas d’étude d’une mission d’attaque de système de pompage d’eauCritical industrial systems are prime targets of cyber threats. In particular the Advanced Persistent Threats (APT) are sophisticated and well-resourced attacks targeting valuable assets. For APTs both the attack and the defense require advanced planning and strategies similar to military operations. The existing cyber-security-aware methodologies achieve valuable results for regular cyberthreats, however they fail to adequately address APTs due to their refined strategies and evasive tactics. The Operational Design methodology of military forces helps in better understanding how APTs devise their strategies. This mission-driven methodology adapted to the APT context relies on the federationof several processes of specification, modeling and analysis in order to produce an operational strategy. To evaluate this approach, a complete federation framework has been developed and applied to the case study of a mission of attack on a water pumping station
6
Obeid, Fadi. "Validation formelle d'implantation de patrons de sécurité." Thesis, Brest, École nationale supérieure de techniques avancées Bretagne, 2018. http://www.theses.fr/2018ENTA0002/document.
Full textAbstract:
Les architectures de systèmes à logiciel posent des défis pour les experts de sécurité. nombreux travaux ont eu pour objectif d’élaborer des solutions théoriques, des guides méthodologiques et des recommandations, pour renforcer la sécurité et protéger ces systèmes.Une solution proposée est d’intégrer des patrons de sécurité comme solutions méthodologiques à adapter aux spécificités des architectures considérées. Une telle solution est considérée fiable si elle résout un problème de sécurité sans affecter les exigences du système.Une fois un modèle d’architecture implante les patrons de sécurisé, il est nécessaire de valider formellement ce nouveau modèle au regard des exigences attendues. Les techniques de model checking permettent cette validation en vérifiant, d’une part, que les propriétés des patrons de sécurité sont respectées et, d’autre part, que les propriétés du modèle initial sont préservées.Dans ce travail de thèse, nous étudions les méthodes et les concepts pour générer des modèles architecturaux respectant des exigences de sécurité spécifiques. Àpartir d’un modèle d’architecture logicielle, d’une politique de sécurité et d’une librairie des patrons de sécurité, nous souhaitons générer une architecture sécurisée. Chaque patron de sécurité est décrit par une description formelle de sa structure et de son comportement, ainsi qu’une description formelle des propriétés de sécurité associées à ce patron.Cette thèse rend compte des travaux sur l’exploitation de techniques de vérification formelle des propriétés, par model-checking. L’idée poursuivie est de pouvoir générer un modèle d’architecture qui implante des patrons de sécurité, et de vérifier que les propriétés de sécurité, comme les exigences de modèle, sont respectées dans l’architecture résultante.En perspective, les résultats de notre travail pourraient s'appliquer à définir une méthodologie pour une meilleure validation de la sécurité des systèmes industriels comme les SCADASoftware-based architectures pose challenges for security experts. Many studieshave aimed to develop theoretical solutions, methodological guides and recommendations to enhance security and protect these systems.One solution proposed is to integrate security patterns as methodological solutions to adapt to the specificities of the considered architectures. Such a solution is considered reliable if it solves a security problem without affecting systemrequirements. Once an architecture model implements the security patterns, it is necessary to formally validate this new model against the expected requirements. Model checking techniques allow this validation by verifying, on one hand, that theproperties of the security patterns are respected and, on the other hand, that the properties of the initial model are preserved.In this thesis work, we study the methods and concepts to generate architectural models that meet specific security requirements. Starting with a software architecture model, a security policy and a library of security patterns, we want to generate a secure architecture. Each security pattern is described by aformal description of its structure and behavior, as well as a formal description of the security properties associated with that pattern.This thesis reports work on the technical exploitation of formal verification of properties, using model-checking.The idea is to be able to generate an architecture model that implements security patterns, and to verify that the security properties, as well as the model requirements, are respected in the resulting architecture.In perspective, the results of our work could be applied to define a methodology for a better validation of the security of industrial systems like SCADA
7
Girard, Pierre. "Formalisation et mise en œuvre d'une analyse statique de code en vue de la vérification d'applications sécurisées." Toulouse, ENSAE, 1996. http://www.theses.fr/1996ESAE0010.
Full textAbstract:
Dans le domaine de la sécurité informatique, de nombreux travaux théoriques concernent les modèles et les règlements de sécurité en se situant très en amont des systèmes réellement implémentés. Cette thèse s'appuie sur les bases théoriques offertes par ces travaux pour fonder une méthode de vérification statique de logiciels applicatifs. Nous proposons pour cela des algorithmes d'analyse qui s'appliquent aux programmes sources et nous démontrons qu'ils sont corrects en les dérivant d'un modèle de sécurité formel. Ils sont utilisés concrètement pour analyser des programmes écrits en langage C. Après une présentation de la problématique de sécurité informatique, nous effectuons un inventaire des menaces et des attaques récemment constatées et nous montrons qu'il existe un besoin en matière de validation statique de logiciels existants. Nous proposons ensuite une méthodologie de vérification de programmes écrits en langage C par annotation de leur code source puis analyse automatique de celui-ci. Dans une seconde partie, nous cherchons à démontrer la correction des algorithmes d'analyse. Pour cela, nous partons d'un modèle formel de sécurité : le modèle de la causalité. Nous le modifions pour en faire un modèle calculatoire, puis nous l'appliquons à la sémantique opérationnelle d'un langage impératif. Nous démontrons alors que l'analyse de la sécurité, exprimée comme une sémantique non standard du langage, est correcte par rapport au modèle de sécurité. Nous examinons enfin les difficultés pratiques posées par l'analyse statique du langage C. Nous nous attachons à analyser ses particularités en termes de structures de donnée et de structures de contôle. Nous proposons des techniques pour résoudre les problèmes posés, en particulier par les variables de type pointeur et les instructions déstructurantes de type saut inconditionnel.
8
Niang, Mohamed. "Vérification formelle et Simulation pour la Validation du système de contrôle commande des EALE (Équipements d'Alimentation des Lignes Électrifiées)." Thesis, Reims, 2018. http://www.theses.fr/2018REIMS021/document.
Full textAbstract:
La SNCF cherche à mettre en place des solutions innovantes permettant d’améliorer la sécurité et les conditions de travail des chargés d’études lors des travaux d’automatisation. En partant de l’étude théorique du projet jusqu’à sa validation sur site, en passant par la mise en œuvre des programmes, du câblage des armoires, et de leur vérification sur plateforme et en usine, ces différentes tâches s’avèrent souvent être longues, complexes, et répétitives, ce qui a pour effet d’augmenter la charge de travail des chargés d’études. En vue d’améliorer les conditions de travail des chargés d’études, ce projet de recherche vise principalement à améliorer leurs méthodologies de vérification des programmes API (aspects fonctionnels et sécuritaires) et du câblage des armoires électriques. Ce projet intitulé « Vérification formelle et simulation pour la validation des programmes API des EALE » se décompose en deux axes : la vérification hors ligne des programmes API : basée sur une approche formelle, la méthode s’appuie sur une modélisation de l’installation électrique, des programmes API et du cahier de recette dans le model-checker Uppaal. Le principe consiste à vérifier automatiquement si les programmes satisfont aux tests du cahier de recette. la vérification en ligne du câblage des armoires de contrôle/commande/ protection grâce à un simulateur de partie opérative interfacé avec les armoires de contrôle/commande/protection (via une armoire de test). La vérification se fera de manière automatique et en ligne, toujours avec les tests du cahier de recette, et permettra de valider le câblage des armoires et les réglages des appareils de protection numériqueIn order to keep its leadership in French rail market and to improve working conditions of its systems engineers during automation projects, the SNCF (French acronym for National Society of French Railways) wants to develop solutions increasing the productivity. One of these improvements focuses on the current methodology used by the systems engineers to verify and validate the control command system of electrical installations. This task remains one of the most important during an automation project because it is supposed to ensure installations safety, but it should be optimized. Through an industrial thesis financed by SNCF, the aim of this research project is to improve this method and reduce time validation of control command system by providing tools which will help systems engineers to verify and validate quickly and automatically the control command system during any automation project. It is composed of two axes : - Offline verification of PLC programs with model checking - Online validation of electrical cabinets with virtual commissioning
9
Regainia, Loukmen. "Assistance au développement et au test d'applications sécurisées." Thesis, Université Clermont Auvergne (2017-2020), 2018. http://www.theses.fr/2018CLFAC018/document.
Full textAbstract:
Garantir la sécurité d’une application tout au long de son cycle de vie est une tâche fastidieuse. Le choix, l’implémentation et l’évaluation des solutions de sécurité est difficile et sujette a des erreurs. Les compétences en sécurité ne sont pas répondues dans toutes les équipes de développement. Afin de réduire ce manque de compétences en sécurité, les développeurs ont a leurs disposition une multitude de documents décrivant des problèmes de sécurité et des solutions requises (i.e., vulnérabilités, attaques, principes de sécurité, patrons sécurité, etc.). Abstraites et informelles, ces documents sont fournis par des sources différentes et leur nombre est en constante croissance. Les développeurs sont noyés dans une multitude de documents ce qui fait obstruction à leur capacité à choisir, implémenter et évaluer la sécurité d’une application. Cette thèse aborde ces questions et propose un ensemble de méthodes pour aider les développeurs à choisir, implémenter et évaluer les solutions de sécurité face aux problèmes de sécurité. Ces problèmes sont matérialisés par les failles, les vulnérabilités, les attaques, etc. et les solutions fournies par des patrons de sécurité. Cette thèse introduit en premier une méthode pour aider les développeurs dans l’implémentation de patrons de sécurité et l’estimation de leur efficacité face aux vulnérabilités. Puis elle présente trois méthodes associant les patrons de sécurité, les vulnérabilités, les attaques, etc. au sein d’une base de connaissance. Cette dernière permet une extraction automatique de classifications de patrons et améliore la rapidité et la précision des développeurs dans le choix des patrons de sécurité face à une vulnérabilité ou une attaque. En utilisant la base de connaissance, nous présentons une méthode pour aider les développeurs dans la modélisation des menaces ainsi que la générations et l’exécution des cas de test de sécurité. La méthode est évaluée et les résultats montrent que la méthode améliore l’efficacité, la compréhensibilité et la précision des développeurs dans le choix des patrons de sécurité et d’écriture des cas de test de sécuritéEnsuring the security of an application through its life cycle is a tedious task. The choice, the implementation and the evaluation of security solutions is difficult and error prone. Security skills are not common in development teams. To overcome the lack of security skills, developers and designers are provided with a plethora of documents about security problems and solutions (i.e, vulnerabilities, attacks, security principles, security patterns, etc.). Abstract and informal, these documents are provided by different sources, and their number is constantly growing. Developers are drown in a sea of documentation, which inhibits their capacity to design, implement, and the evaluate the overall application security. This thesis tackles these issues and presents a set of approaches to help designers in the choice, the implementation and the evaluation of security solutions required to overcome security problems. The problems are materialized by weaknesses, vulnerabilities, attacks, etc. and security solutions are given by security patterns.This thesis first introduces a method to guide designers implement security patterns and assess their effectiveness against vulnerabilities. Then, we present three methods associating security patterns, attacks, weaknesses, etc. in a knowledge base. This allows automated extraction of classifications and help designers quickly and accurately select security patterns required to cure a weakness or to overcome an attack. Based on this nowledge base, we detaila method to help designers in threat modeling and security test generation and execution. The method is evaluated and results show that the method enhances the comprehensibility and the accuracy of developers in the security solutions choice, threat modeling and in the writing of security test cases
10
Beaudenon, Vincent. "Diagrammes de décision de données pour la vérification de systèmes matériels." Paris 6, 2006. http://www.theses.fr/2006PA066337.
Full textAbstract:
Avec la complexité croissante des systèmes informatiques se pose la question de la mise en oeuvre de méthodes automatiques pour leur vérification formelle. Parmi ces méthodes, le model-checking se fonde sur l'exploration exhaustive du comportement d'un système. Plus celui-ci sera complexe, plus cette exploration se traduira par une explosion combinatoire de l'espace des états du système. Diverses approches ont été proposées pour résoudre ce problème, notamment les méthodes symboliques qui sont bases sur une représentation compacte d'ensembles d'états. Depuis les travaux de R. E. Bryant et la définition des Diagrammes de Décision Binaires (BDD), de nombreuses représentations en DAG d'espaces d'états ont vu le jour, parmi celles-ci, on trouve les Diagrammes de Décision de Données (DDD), qui procurent une représentation compacte d'ensemble d'états et sont pourvus de mécanismes de parcours définis localement pour la réalisation des modifications sur ces états et des opérations ensemblistes. Parallélement, les travaux de G. J. Holzmann ont abouti à la création de l'outil de vérification SPIN, basé sur des méthodes énumératives explicites, pour des systèmes décrits en langage Promela. Ces systèmes sont proches de ceux qui sont utilisés pour la synthèse de haut niveau. Nous proposons une approche de vérification symbolique de systèmes matériels décrits dans un sous-ensemble du langage Promela. La représentation symbolique d'ensembles d'états est basée sur les Diagrammes de Décision de Données qui évitent de d'écrire le système au niveau booléen. Nous présentons d'abord la sémantique du langage Promela ainsi que les DDD puis les mécanismes mis en oeuvre pour la vérification de propriétés de logique CTL. Les conclusions tirées de cette première étape conduisent à proposer l'utilisation des Diagrammes de Décision d'Ensembles (SDD) pour améliorer les performances de la vérification automatique. Nous montrons que, bien que pourvus d'une implémentation et d'une terminologie différentes, il se prévalent du même formalisme que les DDD tout en procurant un étiquetage symbolique des arcs de la structure. Nous expérimentons ensuite cette approche sur des systèmes académiques et sur des systèmes issus d'applications industrielles. Ces expérimentations corroborent nos premiers résultats : les SDD couplés aux méthodes de saturation constituent une alternative sérieuse pour la vérification de systèmes à fort degré de concurrence. Nous proposons des perspectives de recherche pour améliorer encore la vérification de tels systèmes mais également pour introduire le concept de hiérarchie dans la description du système
11
Jovanovic, Aleksandra. "Vérification parametrée de systèmes temporisés." Ecole centrale de Nantes, 2013. http://www.theses.fr/2013ECDN0036.
Full textAbstract:
Dans cette thèse, nous étudions la vèrification formelle des systèmes avec des contraintes temporelles. Comme formalisme pour la modélisation et l’analyse de ces systèmes, nous utilisons les automates temporisés. Le model-checking est une méthode de vérification formelle qui vérifie automatiquement si un modèle d’un système donné satisfait une propriété. Cependant, cette méthode nécessite une connaissance complète du système, ce qui est souvent difficile dans les premiers stades de la conception. L’approche paramétrique est un moyen de résoudre ce problème et d’augmenter la robustesse de la conception. Nous étudions les automates temporisés paramétrés, un modèle qui permet l’utilisation d’expressions paramétriques au lieu de valeurs temporelles concrètes dans le modèle. Nous offrons de nouveaux résultats de décidabilité négatifs concernant les propriétés d’accessibilité et d’inévitabilité. Nous proposons alors une nouvelle approche, dans laquelle nous limitons les valeurs des paramètres à des entiers bornés et nous proposons des algorithmes symboliques pour la synthèse de paramètres basée sur le calcul de l’enveloppe entière des états symboliques. Ces algorithmes sont implémentés dans notre outil Roméo. Nous étudions ensuite les jeux temporisés, un modèle utilisé pour les problèmes de contrôle sur des systèmes temps réel et proposons leur paramétrisation. Nous offrons une sous-classe pour laquelle le jeu d’accessibilité est décidable et un algorithme pour le calcul des états gagnants et la synthèse des paramètresIn this thesis we are studying formal verification of systems with timing constraints. As a formalism for modeling and analyzing such systems, we are using timed automata. Model-checking is a formal verification method that automatically verifies whether the model of the system satisfies some property. This method, however, requires complete knowledge of the system, which is often difficult to provide in the early design stages. Parametric approach is a way to address this issue and to increase the robustness of the design. We study parametric timed automata, a model that allows the use of parametric expressions instead of concrete timing values in the model. We offer new negative decidability results concerning reachability and unavoidability properties. We then propose a novel approach, we restrict parameter values to bounded integers and offer symbolic algorithms for parameter synthesis based on the computation of the integer hull of symbolic states. These algorithms are implemented in our tool Roméo. We then study timed game automata, a model used for control problems on real-times systems and propose its parametrization. We offer a subclass for which the reachability game is decidable and an algorithm for the computation of winning states and parameter synthesis. Finally, we study a parametric version of interrupt timed automata, a subclass of hybrid automata that uses stopwatches. We prove that the reachability problem is decidable without any restrictions and we give the complexity bounds
12
Jacquemard, Florent. "Modèles d'automates d'arbres étendus pour la vérification de systèmes infinis." Habilitation à diriger des recherches, École normale supérieure de Cachan - ENS Cachan, 2011. http://tel.archives-ouvertes.fr/tel-00643595.
Full textAbstract:
Ce document présente l'étude de plusieurs modèles de machines à états finis qui étendent tous le même formalisme: les automates d'arbres classiques, et leur application dans différentes tâches telles que l'analyse statique de programmes ou de systèmes, la typage, la vérification de la cohérence de spécifications, le model checking... Les arbres sont une structure naturelle de données, très répandue en informatique, par exemple pour la représentation des structures de données hiérarchiques ou imbriquées, pour des algorithmes spécifiques (arbres binaires de recherche, algorithmes distribués), comme modèle abstrait pour des données semi-structurées utilisées pour l'échange d'information dans le Web, pour une présentation algébrique de processus récursifs, comme les termes en logique... Lorsqu'il s'agit de raisonner sur des systèmes manipulant des arbres, ou modelisés par des arbres, il est crucial d'avoir une représentation finie d'ensembles infinis d'arbres. Les automates d'arbres sont des machines à états finis permettant une telle représentation. Ils ont fait la preuve de leur adéquation à des tâches de raisonnement: ils ont un modèle théorique bien établi, en étroite relation avec la logique, ils bénéficient de bonnes propriétés de composition et d'algorithmes de décision efficaces. En particulier, les automates d'arbres sont utilisées au coeur de systèmes de vérification formelle d'outils de déduction automatique. Toutefois, les automates d'arbres ont des limitations sévères en expressivité. Par exemple, ils sont incapables de faire du filtrage non-linéaire ou d'exprimer des contraintes d'intégrité tels que les clés dans les bases de données. Certaines extensions ont été proposées afin d'améliorer le modèle en essayant de conserver de bonnes propriétés. Nous présentons dans ce document de plusieurs de telles extensions, leurs propriétés et leur utilisation en vérification symbolique de systèmes et de programmes.
13
Boisseau, Alexandre. "Abstractions pour la vérification de propriétés de sécurité de protocoles cryptographiques." Cachan, Ecole normale supérieure, 2003. https://theses.hal.science/tel-01199555.
Full textAbstract:
Depuis le développement de l'utilisation des réseaux informatiques et de l'informatisation des communications, il est apparu pour le public un besoin de sécuriser les communications électroniques. Les considérations cryptographiques constituent un élément de réponse au problème de la sécurité des communications et les protocoles cryptographiques décrivent comment intégrer la cryptographie à l'intérieur de communications réelles. Cependant, même dans le cas où les algorithmes de chiffrement sont supposés robustes, les protocoles peuvent présenter des failles de conception exploitables (failles logiques), entrainant un besoin de vérification formelle. Dans cette thèse, nous utilisons des techniques d'abstraction afin de prouver formellement divers types de propriétés. Les propriétés de secret et d'authentification, les propriétés de type équité et des propriétés de type anonymatSince the development of computer networks and electronic communications, it becomes important for the public to use secure electronic communications. Cryptographic considerations are part of the answer to the problem and cryptographic protocols describe how to integrate cryptography in actual communications. However, even if the encryption algorithms are robust, there can still remain some attacks due to logical flaw in protocols and formal verification can be used to avoid such flaws. In this thesis, we use abstraction techniques to formally prove various types of properties : secrecy and authentication properties, fairness properties and anonymity
14
Kamsu-Foguem, Bernard. "Modélisation et vérification des propriétés de systèmes complexes : Application aux processus d'entreprise." Montpellier 2, 2004. http://www.theses.fr/2004MON20050.
Full text
15
Rasse, Alban. "Une Approche Orientée Modèles pour la Spécification, la Vérification et l’Implantation des Systèmes Logiciels Critiques." Mulhouse, 2006. https://www.learning-center.uha.fr/opac/resource/une-approche-orientee-modeles-pour-la-specification-la-verification-et-limplantation-des-systemes-lo/BUS3944436.
Full textAbstract:
La conception des applications logicielles est une tâche délicate qui requiert la prise en compte d'un ensemble d’aspects (concurrence, communication, comportement hybride,…) et l’intégration d’un ensemble d’activités particulières. Le travail présenté dans ce manuscrit, tire partie de l'Ingénierie Dirigée par les Modèles (IDM), d'UML, des méthodes formelles, des systèmes multi-agents et des frameworks afin de proposer un processus de conception intégrant des aspects de spécification, de vérification et d'implantation. Il se fonde sur la réalisation de trois modèles adaptés à chacune de ces activités : le modèle de spécification, le modèle de vérification et le modèle d'implantation (Figure 1). Dans ce contexte, l’Ingénierie Dirigée par les Modèles offre les concepts (métamodélisation et transformations de modèles) nécessaires à l’intégration et à la manipulation de ces trois modèles au sein de l'approche proposée. En outre, les transformations de modèles permettent de réaliser la projection d'un modèle source vers différents domaines afin de profiter de leurs avantages respectifs; à partir du modèle de spécification, il est alors possible d'obtenir les modèles de vérification et d'implantation. Le modèle de spécification permet de représenter une abstraction des systèmes logiciels réactifs concurrents ; il est décrit à l’aide d’un Langage Spécifique de Domaine (ou DSL) inspiré des ADL et des diagrammes de composants d’UML 2. 0. Il repose sur l'utilisation d'agents concurrents, qui communiquent à l'aide d'actions partagées et d'objets partagés ; leur comportement est conforme à une sémantique d’exécution hybride (événementiel asynchrone et continu synchrone). Le modèle de vérification permet au concepteur d’utiliser des méthodes et des techniques de vérification qui garantissent que le modèle obtenu durant la phase de spécification est conforme au comportement souhaité. En effet, dans le cas de systèmes critiques, les aspects de vivacité et de sûreté de fonctionnement sont primordiaux. Pour garantir ces aspects, nous proposons de recourir à des spécifications formelles et à des techniques formelles de vérification en modélisant le modèle de vérification à l’aide d’une algèbre de processus nommée Finite State Processes (ou FSP) pouvant être exploitée par l'outil de model-checking LTSA. Le modèle d’implantation est exprimé à l'aide de classes et de configurations d’objets; il repose sur l’utilisation d’un framework Java qui fournit un ensemble de concepts et une sémantique d’exécution proches de ceux utilisés dans le modèle de spécification. Ce faisant il permet de réduire l’écart sémantique entre la réalisation et la conception précédemment vérifiée.
16
Lewicki, Alexandre. "Conception de modèles haut niveau pour l'optimisation et la vérification de systèmes Bluetooth." Nice, 2008. http://www.theses.fr/2008NICE4110.
Full textAbstract:
Les différents travaux de recherche présentés dans cette thèse portent sur la conception de modèles fonctionnels à haut niveau d’abstraction ainsi que leur utilisation dans un flot de conception de systèmes sans fil. La Méthodologie de Conception des Systèmes Embarqués (MCSE) a été expérimentée pour la conception des circuits et systèmes dédiés à la technologie Bluetooth. La première partie de la thèse présente la méthodologie MCSE et son application dans la conception d’un système comportant un capteur de température distant et relié par Bluetooth. A partir des spécifications de l’application, les modèles fonctionnels ont été élaborés et raffinés après différentes étapes successives. Les modèles ont ensuite été traduits à l’aide de SystemC, une librairie C++ permettant de décrire les systèmes aux niveaux matériels et logiciels. Les modèles ont ensuite été exploités dans le cadre de simulation de réseaux sans fil. Ces résultats peuvent être utilisés suivant 3 différents axes : l’analyse de protocole, l’analyse de performances et l’exploration d’architecture. La deuxième partie du travail a été d’introduire les modèles fonctionnels dans le cadre d’un environnement de vérification matérielle avant fabrication. Deux environnements ont été mis en place pour les concepteurs du circuit ainsi que pour les ingénieurs de vérification. Cette technique permet de simuler et stresser le circuit de manière plus avancée, notamment grâce à la possibilité d’écrire des tests plus completsThe different works conducted in this thesis were to design high level functional models that were used in a wireless system design flow. The MCSE methodology was followed to design those models and the results have been used for Bluetooth technology system design and verification. The first part of the work presents the MCSE methodology that has been used for the design of the models. Starting from the specification of a concrete use case, a temperature sensor, we designed a functional model of the system with successive refinement steps. The models were then translated in SystemC, a C++ library that allows describing both hardware and software parts of a system. The results of the exploitation of the models in a wireless network simulation can be used for protocol analysis, performance analysis and performance exploration. The second part of the work was to introduce the functional models in a hardware verification environment. Two different techniques for design engineers and verification engineers have been settled. This technique brings enhanced verification features with the possibility to write complex tests
17
Sangnier, Arnaud. "Vérification de systèmes avec compteurs et pointeurs." Cachan, Ecole normale supérieure, 2008. http://www.theses.fr/2008DENS0051.
Full textAbstract:
Au cours des dernières années, les méthodes formelles se sont avérées être une approche prometteuse pour garantir que le comportement d’un système informatique respecte une spécification donnée. Parmi les différentes techniques développées, le model-checking a été récemment étudié et appliqué avec succès à un grand nombre de modèles comme les systèmes à compteurs, les automates communicants (avec perte), les automates à pile, les automates temporisés, etc. Dans cette thèse, nous considérons deux modèles particuliers dans l’objectif de vérifier des programmes manipulant des variables entières et des variables de pointeurs. Dans une première partie, nous nous intéressons aux systèmes à compteurs. Nous commençons par définir ce modèle ainsi que ses différentes restrictions. Nous introduisons ensuite une sous-classe de systèmes à compteurs, appelée les machines à compteurs reversal-bornées, pour lesquelles de nombreux problèmes d’accessibilité sont décidables. Nous montrons que cette classe peut être étendue tout en gardant les résultats de décidabilité et nous prouvons qu’il est possible de décider si un Système d’Addition de Vecteurs avec États est reversal-borné, alors que cela n’est pas possible si l’on considère les systèmes à compteurs dans leur généralité. Nous finissons cette partie sur les systèmes à compteurs par l’étude de problèmes de model-checking de logiques temporelles. Les logiques temporelles que nous prenons en compte permettent de parler des données manipulées par le système. En particulier, nous montrons que le model-checking d’automates à un compteur déterministes avec des formules de la logique LTL avec registres est décidable, mais que cela n’est plus vrai lorsque l’hypothèse sur le déterminisme est supprimée. Dans une deuxième partie, nous introduisons le modèle des systèmes à pointeurs, qui est utilisé pour représenter des programmes manipulant des listes simplement chaînées. Nous donnons un algorithme qui traduit tout système à pointeurs en un système à compteurs qui lui est bisimilaire. Ceci nous permet de réutiliser les méthodes existantes pour l’analyse de systèmes à compteurs pour vérifier des programmes avec listes. Nous présentons ensuite une extension de la logique CTL* pour vérifier des propriétés temporelles sur de tels programmes, et nous étudions la décidabilité du problème de model-checking pour cette nouvelle logique. Finalement, dans une dernière partie, nous donnons une description de l’outil TOPICS (Translation of Programs Into Counter Systems) qui traduit un programme écrit dans un fragment syntaxique du langage C en un système à compteursIn the past years, formal methods have shown to be a succesfull approach to ensure that the behavior of an informatic system will respect some properties. Among the different existing techniques, model-checking have been recently studied and successfully applied to a lot of models like counter systems, lossy channel systems, pushdown automata, timed automata, etc. In this thesis, we consider two different models to verify programs which manipulate integer variables and pointer variables. In a first part, we deal with counter systems. We define the model and the different restrictions which have been proposed. We then introduce a restricted class of counter systems, called the reversal-bounded counter machines, for which many reachability problems are decidable. We show that this class can be extended keeping the decidability results and we prove that we can decide whether a Vector Addition System with States is reversal-bounded or not, which is not possible for general counter systems. We then study the problem of model-checking counter systems with different temporal logics. The temporal logics we consider allow to speak about the data manipulated by the system. In particular, we show that the model-checking of deterministic one-counter automata with formulae of LTL with registers is decidable, and becomes undecidable when considering non deterministic one-counter automata and two counter automata. In a second part, we introduce the model of pointer systems, which is used to represent programs manipulating single linked lists. We propose an algorithm to translate any pointer system into a bisimilar counter system. This allows us to reuse existing techniques over counter systems to analyze these programs. We then propose an extension of CTL* to verify temporal properties for such programs, and we study the decidability of the model-checking problem for this new logic. Finally we present the tool TOPICS (Translation of Programs Into Counter Systems) which translates a C-like program with pointers and integer variables into a counter system
18
Leildé, Vincent. "Aide au diagnostic de vérification formelle de systèmes." Thesis, Brest, École nationale supérieure de techniques avancées Bretagne, 2019. http://www.theses.fr/2019ENTA0011.
Full textAbstract:
Le model checking est une technique de vérification formelle qui consiste à certifier que le comportement d’un système formel satisfait des propriétés formelles. Son principe est d’explorer l’ensemble des exécutions possibles du système pour découvrir des chemins d’exécution (traces) violant les propriétés. Si c’est le cas, l’ingénieur doit remonter aux causes qui ont produit la trace. L’objectif de la thèse est d’assister l’ingénieur lors de cette phase que l’on appelle diagnostic. Nous proposons un cadre combinant différents types de connaissances et activités cognitives, supporté par une méthode et une infrastructure. Nous illustrons l’approche sur la sécurisation d’un système SCADA. Quand le diagnosticien est vérificateur du modèle, il doit faire face à des traces de grande taille. Il réalise un diagnostic en mobilisant une multitude d’activités cognitives complexes. Pour les outiller, nous proposons une classification de ces activités selon la taxonomie de Bloom. Quand la cause réelle opère sur des connaissances autres que celles du model checking, ces moyens sont alors insuffisants. Quand le diagnosticien est le concepteur du modèle, il dispose ou non de connaissances de domaine permettant de le débloquer en lui offrant des nouveaux regards sur la trace. Pour y parvenir, il faut disposer du domaine et corréler les connaissances du domaine et du model checking pour réduire leur fossé sémantique. Nous proposons des structures pour capturer et réutiliser le domaine. D’un côté le problem case formule le problème que l’on cherche à résoudre et permet de préciser le diagnostic de la solution construite. D’un autre côté les sample, pattern et component cases capturent des éléments de solutions et permettent d’isoler le diagnostic. Quand le diagnosticien est l’architecte du système, il combine des éléments de problèmes et de solutions provenant à la foisde l’ingénierie du domaine et de l’application. Pour progresser de manière fluide dans la solution et enrichir les propriétés à vérifier, nous proposons une méthode de résolution de problème. Alimentée par la base de connaissances issue du domaine, celle-ci réalise des allers-retours entre l’espace du problème et l’espace de la solution, traçant problèmes et solutions choisies, et augmentant la vérification et le diagnostic grâce à de nouvelles propriétés. De manière transversale aux autres phases, le processus de vérification doit être organisé. Nous proposons une infrastructure permettant d’organiser, capitaliser et réutiliser les diverses connaissances (model checking, domaine, méthode). L'infrastructure est divisée en trois niveaux, le niveau physique regroupe les données brutes, le niveau connaissance regroupe des ontologies, et le niveau d’accès fournit des interactions supportées par les connaissances, dont les activités cognitives de diagnostic, organisées suivant la taxonomie de Bloom. Nous proposons un outil de simplification de traces par facettes reposant sur cette infrastructureModel checking is a formal verification technique verifying that a system behavior satisfies formal properties. This technique explores all the possible executions of the system to discover execution paths (traces) violating formal properties. When a property is violated, the engineer must find the root causes that produced the trace. The goal of this work is to assist the engineer during this phase, which is called diagnosis. Our proposition is a framework combining various kinds of knowledge and cognitive activities, supported by a method and an infrastructure. We apply the approach to securing a SCADA system. When the diagnostician is the model verifier, he generally faces large traces. The diagnosis is obtained by mobilizing a multitude of complex cognitive activities. To tool these activities, we propose to classify them according to the Bloom’s taxonomy. Even so, these means are insufficient when the real cause doesn’t operate on model checking knowledge. When the diagnostician is the model designer, he may or may not have domain knowledge. This knowledge offers new perspectives about the trace, and may unblock the diagnosis. We propose a structure to capture and reuse this knowledge. Correlations can be explicited o reduce the semantic gap between domain and model checking knowledge. On the one hand, the problem case formulates the problem to be solved, and precises the diagnosis of the constructed solution. On the other hand, the sample, pattern and component cases capture elements of solutions, and isolate the diagnosis. When the diagnostician is the system architect, he combines elements of problemsand solutions from both domain and application engineering. To progress smoothly in the solution and enrich the properties to be checked, we propose a problem solving method. Fed by the domain knowledge base, the method goes back and forth between the problem space and the solution space, tracing chosen problems and solutions, and facilitating verification and diagnosis thanks to new properties. We propose an infrastructure to organize, share and reuse various knowledge implied during the verification process (model checking, domain, method). This infrastructure is divided into three levels, the physical level gathers the raw data, the knowledge level gathers ontologies, and the access level provides interactions supported by knowledge. We offer a trace simplification tool diagnosis based on facets, and promoted by our infrastructure
19
Pascual, Nathalie. "Horloges de synchronisation pour systèmes haute sécurité." Montpellier 2, 1992. http://www.theses.fr/1992MON20145.
Full textAbstract:
La participation de l'aerospatiale au pole firtech microelectronique du grand sud ouest est a l'origine de ce travail. La tendance actuelle est a une utilisation de plus en plus importante des calculateurs et des systemes informatiques. Des lors que de tels systemes sont charges d'un role de securite, la notion de calculateurs tolerants aux fautes prend alors toute sa signification. C'est dans le cadre de la securite que s'inscrit le travail presente dans ce memoire, il concerne plus precisement la distribution tolerante aux fautes de signaux d'horloge aux diverses unites de traitement et de commandes redondantes. Le dispositif elabore sera utilise pour synchroniser des acquisitions de donnees au niveau de capteurs ou pour generer des commandes et etre sur que les donnees manipulees sont correctes et que les commandes vont s'appliquer. Deux asics sont issus de ce travail. Le circuit horloge est capable de detecter, signaler la presence de deux pannes et de se reconfigurer sans perte du synchronisme global
20
Schnepf, Nicolas. "Orchestration et vérification de fonctions de sécurité pour des environnements intelligents." Thesis, Université de Lorraine, 2019. http://www.theses.fr/2019LORR0088/document.
Full textAbstract:
Les équipements intelligents, notamment les smartphones, sont la cible de nombreuses attaques de sécurité. Par ailleurs, la mise en œuvre de mécanismes de protection usuels est souvent inadaptée du fait de leurs ressources fortement contraintes. Dans ce contexte, nous proposons d'utiliser des chaînes de fonctions de sécurité qui sont composées de plusieurs services de sécurité, tels que des pare-feux ou des antivirus, automatiquement configurés et déployés dans le réseau. Cependant, ces chaînes sont connues pour être difficiles à valider. Cette difficulté est causée par la complexité de ces compositions qui impliquent des centaines, voire des milliers de règles de configuration. Dans cette thèse, nous proposons l'architecture d'un orchestrateur exploitant la programmabilité des réseaux pour automatiser la configuration et le déploiement de chaînes de fonctions de sécurité. Il est important que ces chaînes de sécurité soient correctes afin d’éviter l'introduction de failles de sécurité dans le réseau. Aussi, notre orchestrateur repose sur des méthodes automatiques de vérification et de synthèse, encore appelées méthodes formelles, pour assurer la correction des chaînes. Notre travail appréhende également l'optimisation du déploiement des chaînes dans le réseau, afin de préserver ses ressources et sa qualité de serviceSmart environments, in particular smartphones, are the target of multiple security attacks. Moreover, the deployment of traditional security mechanisms is often inadequate due to their highly constrained resources. In that context, we propose to use chains of security functions which are composed of several security services, such as firewalls or antivirus, automatically configured and deployed in the network. Chains of security functions are known as being error prone and hard to validate. This difficulty is caused by the complexity of these constructs that involve hundreds and even thousands of configuration rules. In this PhD thesis, we propose the architecture of an orchestrator, exploiting the programmability brought by software defined networking, for the automated configuration and deployment of chains of security functions. It is important to automatically insure that these security chains are correct, before their deployment in order to avoid the introduction of security breaches in the network. To do so, our orchestrator relies on methods of automated verification and synthesis, also known as formal methods, to ensure the correctness of the chains. Our work also consider the optimization of the deployment of chains of security functions in the network, in order to maintain its resources and quality of service
21
Turuani, Mathieu. "Sécurité des protocoles cryptographiques : décidabilité et complexité." Nancy 1, 2003. http://www.theses.fr/2003NAN10223.
Full text
22
Dacier, Marc. "Vers une évaluation quantitative de la sécurité informatique." Phd thesis, Institut National Polytechnique de Toulouse - INPT, 1994. http://tel.archives-ouvertes.fr/tel-00012022.
Full textAbstract:
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.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.
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.
23
Ziani, Rezki. "Vérification des objectifs de disponibilité et de maintenabilité des systèmes complexes modélisés par leurs ensembles minimaux : vers une optimisation de la sûreté des systèmes." Compiègne, 1986. http://www.theses.fr/1986COMPI250.
Full textAbstract:
Étant donné un système, l’utilisateur demande à ce système qu’il satisfasse à ses besoins avec des garanties suffisantes. Le constructeur répond par des performances mais rencontre des difficultés à démontrer les garanties. Dans ce travail, nous développons une méthodologie rigoureuse aidant le constructeur à démontrer les garanties, à confirmer la bonne conception du système et/ou indiquer les recommandations favorables. Un modèle de vérification à objectifs de sûreté pour un système en phase conception est proposé. Pour rendre réalistes les actions d’amélioration qui peuvent être proposés, ce modèle est généralisé à un modèle d’optimisation avec contrainte économique.
24
Addouche, Nawal. "Damrts : une méthodologie pour la vérification formelle des propriétés de sûreté de fonctionnement de systèmes temps réel." Grenoble INPG, 2006. http://www.theses.fr/2006INPG0034.
Full textAbstract:
Le rapport de thèse présente une méthodologie d'analyse des systèmes temps réel qui propose à l'analyste un moyen de contourner les difficultés de la modélisation formelle pour vérifier formellement les propriétés de sûreté de fonctionnement (SdF) du système. D'un point de vue pratique, nous avons défini la méthodologie DAMRTS (Dependability Analysis Models for Real-Time Systems) dont les trois étapes principales sont basées sur la proposition d'une démarche d'analyse et de modélisation, la réalisation d'un translateur automatique « modèles UMU modèles formels» et enfin, la vérification des propriétés de SdF via un model checker. Pour obtenir un modèle de systèmes temps réel qui représente les aspects fonctionnels et dysfonctionnels du système, nous avons défini, puis construit à l'aide de l'outil de métamodélisation GME, le profil DAMRTS. En plus des contraintes temporelles propres à ce type de système, ce dernier permet la modélisation des données qualitatives et quantitatives de SdF. Le comportement du système est décrit par deux types de machines d'états UML étendues; il s'agit de machines d'états stochastiques et de machines d'états temps réel probabilistes destinées respectivement à être translatées vers des chaînes de Markov à temps continu et des automates temporisés probabilistes. Ces modèles formels sont exploités pour la vérification des propriétés de SdF grâce au model checker probabiliste PRISM. Enfin, nous avons illustré notre proposition à travers l'analyse de SdF d'une chaîne d'assemblage de micro-moteurs. L'exemple est extrait d'un projet Européen nommé PABADIS (Plant Automation Based on Distributed Systems) développé au sein du laboratoire LGI2PLn the thesis report, we present a methodology dedicated to the analysis of real time systems which provides the analyst with a means to get round the difficulties of formai modelling for formally checking the dependability properties of system. From a practical point of view, we have defined the methodology DAMRTS (Dependability Analysis Models for Real-Time Systems) whose the three main stages are based on an analysis and modelling process, the realization of an automatic translator« UML models formal models» and finally, the verification of dependability properties via a model checker. To achieve a model of a real time system which represents both functional and dysfunctional aspects of the system, we have defined then built the profile DAMRTS using the tool of metamodelling GME. Ln additior to the specific temporal constraints inherent to real time systems, this profile allows modelling qualitative and quantitative data relative to the dependability of the system. The system behaviour is described by two types of extended UML statecharts : the stochastic statecharts and the probabilistic real time statecharts respectively intended to be translated towards continuous time Markov chains and probabilistic timed automata. These formal models are then exploited for the verification of dependability properties via the probabilistic model checkel PRISM. Lastly, we illustrated our proposai through the dependability analysis of an automated chain assembly of micro-motors. The example is excerpted from a European project named PABADIS (Plant Automation Based on Distributed Systems) developed at the LGI2P laboratory
25
Gascard, Eric. "Méthodes pour la vérification formelle de systèmes matériels et logiciels à architecture régulière." Aix-Marseille 1, 2002. http://www.theses.fr/2002AIX11047.
Full textAbstract:
Le cadre de cette thèse est l'utilisation des méthodes formelles pour la spécification et la validation de systèmes matériels et logiciels. Nos travaux se sont concentrés sur la validation formelle de systèmes à architecture régulière et paramétrable, circuits combinatoires itératifs d'une part, et applications distribuées s'exécutant sur des réseaux d'interconnexion symétriques d'autre part. La première partie de cette thèse est consacrée à la vérification formelle automatique de circuits à structure répétitive régulière. Un modèle de fonctions récursives est utilisé, le processus de preuve mettant en jeu des techniques inductives permet un raisonnement générique sur la taille du circuit. Le résultat présenté ici est une heuristique de généralisation de théorèmes inductifs spécialisée pour les modèles fonctionnels considérés. Cette méthode permet de produire les théorèmes généralisés ainsi que certains lemmes intermédiaires et d'automatiser ainsi le processus de vérification. La seconde partie propose une méthode de modélisation et de validation de programmes distribués sur les réseaux d'interconnexion symétriques. Les preuves sont ici paramétrées sur l'ordre du réseau (nombre de processeurs). Le modèle formel choisi pour la représentation des réseaux dans l'environnement de démonstration automatique est basé sur le concept de graphe de Cayley. Notre méthode prend en compte les opérations de communications collectives (diffusion, distribution, réduction) utilisées par les applications distribuées. La modélisation et la méthode de preuve développées permettent entre autres de s'abstraire du problème des communications point à point, et de raisonner au niveau du processeur. De plus, elle permet d'obtenir automatiquement les invariants nécessaires au preuves.
26
Nguyên, Duy-Tùng. "Vérification symbolique de modèles à l'aide de systèmes de ré-écriture dédiés." Phd thesis, Université d'Orléans, 2010. http://tel.archives-ouvertes.fr/tel-00579490.
Full textAbstract:
Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles.
27
Li, Letitia. "Approche orientée modèles pour la sûreté et la sécurité des systèmes embarqués." Thesis, Université Paris-Saclay (ComUE), 2018. http://www.theses.fr/2018SACLT002/document.
Full textAbstract:
La présence de systèmes et d'objets embarqués communicants dans notre vie quotidienne nous a apporté une myriade d'avantages, allant de l'ajout de commodité et de divertissement à l'amélioration de la sûreté de nos déplacements et des soins de santé. Cependant, les défauts et les vulnérabilités de ces systèmes exposent leurs utilisateurs à des risques de dommages matériels, de pertes financières, et même des dommages corporels. Par exemple, certains véhicules commercialisés, qu'ils soient connectés ou conventionnels, ont déjà souffert d'une variété de défauts de conception entraînant des blessures et la mort. Dans le même temps, alors que les véhicules sont de plus en plus connectés (et dans un avenir proche, autonomes), les chercheurs ont démontré la possibilité de piratage de leurs capteurs ou de leurs systèmes de contrôle interne, y compris l'injection directe de messages sur le bus CAN.Pour assurer la sûreté des utilisateurs et des passants, il faut considérer plusieurs facteurs. La sûreté conventionnelle suggère qu'un système ne devrait pas contenir de défauts logiciels et matériels qui peuvent l'empêcher de fonctionner correctement. La "sûreté de la fonction attendue" consiste à éviter les situations que le système ou ses composants ne peuvent pas gérer, comme des conditions environnementales extrêmes. Le timing peut être critique pour certains systèmes en temps réel, car afin d'éviter des situations dangereuses, le système devra réagir à certains événements, comme l'évitement d'obstacles, dans un délai déterminé. Enfin, la sûreté d'un système dépend de sa sécurité. Un attaquant qui peut envoyer des commandes fausses ou modifier le logiciel du système peut changer son comportement et le mettre dans diverses situations dangereuses. Diverses contre-mesures de sécurité et de sûreté pour les systèmes embarqués, en particulier les véhicules connectés, ont été proposées. Pour mettre en oeuvre correctement ces contre-mesures, il faut analyser et vérifier que le système répond à toutes les exigences de sûreté, de sécurité et de performance, et les faire la plus tôt possible dans les premières phases de conception afin de réduire le temps de mise sur le marché, et éviter les reprises. Cette thèse s'intéresse à la sécurité et la sûreté des les systèmes embarqués, dans le contexte du véhicule autonome de l'Institut Vedecom. Parmi les approches proposées pour assurer la sûreté et la sécurité des les systèmes embarqués, l'ingénierie dirigée par modèle est l'une de ces approches qui couvre l'ensemble du processus de conception, depuis la définition des exigences, la conception du matériel et des logiciels, la simulation/vérification formelle et la génération du code final. Cette thèse propose une méthodologie de modélisation pour une conception sûre et sécurisée, basée sur la méthodologie SysML-Sec, qui implique de nouvelles méthodes de modélisation et de vérification. La modélisation de la sécurité est généralement effectuée dans les dernières phases de la conception. Cependant, la sécurité a un impact sur l'architecture/allocation; les décisions de partitionnement logiciel/matériel devraient être prises en fonction de la capacité de l'architecture à satisfaire aux exigences de sécurité. Cette thèse propose comment modéliser les mécanismes de sécurité et l'impact d'un attaquant dans la phase de partitionnement logiciel/matériel. Comme les protocoles de sécurité ont un impact négatif sur le performance d'un système, c'est important de mesurer l'utilisation des composants matériels et les temps de réponse du système. Des composants surchargés peuvent entraîner des performances imprévisibles et des retards indésirables. Cette thèse traite aussi des mesures de latence des événements critiques pour la sécurité, en se concentrant sur un exemple critique pour les véhicules autonomes : le freinage/réponse après la détection d'obstacles. Ainsi, nos contributions soutiennent la conception sûre et sécurisée des systèmes embarquésThe presence of communicating embedded systems/IoTs in our daily lives have brought a myriad of benefits, from adding conveniences and entertainment, to improving the safety of our commutes and health care. However, the flaws and vulnerabilities in these devices expose their users to risks of property damage, monetary losses, and personal injury. For example, consumer vehicles, both connected and conventional, have succumbed to a variety of design flaws resulting in injuries and death. At the same time, as vehicles are increasingly connected (and in the near future, autonomous), researchers have demonstrated possible hacks on their sensors or internal control systems, including direct injection of messages on the CAN bus.Ensuring the safety of users or bystanders involves considering multiple factors. Conventional safety suggests that a system should not contain software and hardware flaws which can prevent it from correct function. `Safety of the Intended Function' involves avoiding the situations which the system or its components cannot handle, such as adverse extreme environmental conditions. Timing can be critical for certain real-time systems, as the system will need to respond to certain events, such as obstacle avoidance, within a set period to avoid dangerous situations. Finally, the safety of a system depends on its security. An attacker who can send custom commands or modify the software of the system may change its behavior and send it into various unsafe situations. Various safety and security countermeasures for embedded systems, especially connected vehicles, have been proposed. To place these countermeasures correctly requires methods of analyzing and verifying that the system meets all safety, security, and performance requirements, preferably at the early design phases to minimize costly re-work after production. This thesis discusses the safety and security considerations for embedded systems, in the context of Institut Vedecom's autonomous vehicle. Among the proposed approaches to ensure safety and security in embedded systems, Model-Driven Engineering is one such approach that covers the full design process, from elicitation of requirements, design of hardware and software, simulation/formal verification, and final code generation. This thesis proposes a modeling-based methodology for safe and secure design, based on the SysML-Sec Methodology, which involve new modeling and verification methods. Security modeling is generally performed in the last phases of design. However, security impacts the early architecture/mapping and HW/SW partitioning decisions should be made based on the ability of the architecture to satisfy security requirements. This thesis proposes how to model the security mechanisms and the impact of an attacker as relevant to the HW/SW Partitioning phase. As security protocols negatively impact performance, it becomes important to measure both the usage of hardware components and response times of the system. Overcharged components can result in unpredictable performance and undesired delays. This thesis also discusses latency measurements of safety-critical events, focusing on one critical to autonomous vehicles: braking as after obstacle detection. Together, these additions support the safe and secure design of embedded systems
28
Abou, El Kalam Anas. "Modèles et politiques de sécurité pour les domaines de la santé et des affaires sociales." Toulouse, INPT, 2003. http://www.theses.fr/2003INPT043H.
Full textAbstract:
Ce mémoire propose une démarche pour définir des politiques de sécurité adaptées aux systèmes d'information et de communication en santé et social (SICSS). Le but de la méthode présentée est de réaliser un bon compromis entre le respect du principe du moindre privilège et la flexibilité du contrôle d'accès. Un nouveau modèle de contrôle d'accès Or-BAC (Organisation-Based Access Control) est également présenté. Or-BAC est capable de spécifier des politiques de sécurité pour les SICSS, comme il peut être adapté à une gamme très large d'applications. Or-BAC est représenté par des diagrammes entité-relation, puis dans deux nouveaux langages logiques. Il est par ailleurs intégré dans une modélisation UML des phases d'authentification et d'autorisation. Un prototype a été développé pour illustrer l'application de la politique de sécurité dans le cas d'un centre dentaire.
29
Ermont, Jérôme. "Une algèbre de processus pour la modélisation et la vérification de systèmes temps-réel avec préemption." Toulouse, ENSAE, 2002. http://www.theses.fr/2002ESAE0024.
Full textAbstract:
La conception et la maîtrise des systèmes embarqués proposent un défi de plus en plus important à relever avec le développement des aéronefs modernes. Cette importance révèle la nécessité de mettre en œuvre des méthodes formelles automatiques permettant d’assister le concepteur. Or, la nature distribuée et le partage des ressources de tels systèmes rendent difficiles leur description à l'aide des méthodes classiques mises en œuvre dans le cadre des systèmes temps-réel (algèbres de processus temporisés, automates temporisés, et, par la suite, de savoir si le système répond bien aux spécifications attendues (vérification). L'objectif de cette thèse est de proposer un élément de réponse à la modélisation, puis à la vérification, de tels systèmes en utilisant les mécanismes de préemption pour réaliser le partage de ressources. L’idée proposée consiste à construire un système embarqué sous la forme d'un ensemble de processus réactifs communicants et préemptibles spécifiés au moyen d’un formalisme algébrique. Deux types de préemption ont été identifiés : l'interruption définitive et la suspension temporaire avec reprise. De ces deux types de préemption découlent la structure de l'étude. En premier lieu, nous proposons de définir une algèbre de processus, nommée TPAPa, permettant l'interruption définitive. Afin de pouvoir vérifier les systèmes décrits dans ce formalisme, une traduction en automates temporisés a été réalisée. De cette manière, il est possible d’utiliser les outils de model-checking classiques (UPPAAL, KRONOS, CMC,. . . ). En deuxième lieu, nous avons intégré la possibilité de suspendre temporairement l'activité d’un processus puis sa reprise à partir du point d’arrét. Cette fois, la traduction conduit au formalisme des automates à chronomètres. Nous montrons alors que la vérification de propriétés sur une algèbre de processus possédant des mécanismes de suspension, nommée TPAPas, est en général indécidable.
30
Constant, Camille. "Génération automatique de tests pour modèles avec variables ou récursivité." Rennes 1, 2008. ftp://ftp.irisa.fr/techreports/theses/2008/constant.pdf.
Full textAbstract:
Nous nous intéressons dans ce document à la génération automatique de tests de conformité pour des implémentations réactives. Nous nous attachons dans un premier temps à étendre la méthode de génération de tests, basée sur la théorie du test de conformité à la ioco, en reliant trois niveaux de description (propriétés, spécification et implémentation). Nous combinons pour cela vérification formelle et test de conformité. Nous obtenons ainsi, lors de l'exécution du cas de test sur l'implémentation, des verdicts pouvant indiquer la non-conformité de l'implémentation, mais également la satisfaction/violation de la propriété par l'implémentation et/ou la spécification. Nous étendons dans un deuxième temps la génération de tests par l'expressivité du modèle de spécification en nous intéressant aux spécifications interprocédurales récursives. Notre méthode est basée sur une analyse exacte de co-accessibilité permettant de décider si et comment un objectif de test pourra être atteint. Cependant, l'incapacité des cas de test récursifs à connaître leur propre pile d'exécution ne permet pas d'utiliser la totalité des résultats de l'analyse. Nous discutons de ce problème d'observation partielle et de ses conséquences puis nous proposons un moyen de minimiser son impact. Enfin, nous expérimentons ces méthodes de génération de tests sur quelques exemples et une étude de casThis thesis adresses the problem of automatic test case generation for testing the conformance of a reactive implementation. We first propose a methodology which extends the testing theory based on the ioco conformance relation by distinguishing three levels of description: properties, specification and implementation. The methogology integrates verification and conformance testing. The execution of the generated test cases on the implementation allows detecting conformance violations between implementation and specification, but also violation/satisfaction of the properties by the implementation or the specification. Secondly, we introduce a more expressive specification model: recursive interprocedural specifications. The test generation method we propose is based on coreachability analysis, which allows deciding whether and how the test purpose can still be satisfied. However, although it is possible to carry out an exact analysis, the inability of test cases to inspect their own stack prevents them from fully using the coreachability information. We discuss this partial observation problem, its consequences, and how to minimise its impact. Finally, we experiment these methods of test generation on several examples and a case study
31
Dragomir, Iulia. "Conception et vérification d'exigences de sûreté temporisées à base de contrats dans les modèles SysML." Toulouse 3, 2014. http://thesesups.ups-tlse.fr/2510/.
Full textAbstract:
De nos jours, les systèmes informatiques croissent en taille et en complexité. Intégrés dans des dispositifs de différents domaines tels que l'avionique, l'aéronautique, l'électronique grand public, etc. , ils sont souvent considérés comme critiques à l'égard de la vie humaine, des coûts et de l'environnement. Concevoir des systèmes embarqués temps-réel critiques sûrs et fiables est une tâche difficile, étant donné que leurs modèles sont souvent source d'erreurs. Une façon pour les concepteurs de contourner cette difficulté consiste à s'appuyer sur la modélisation compositionnelle de composants logiciels pilotée par les exigences. Le raisonnement à base de contrats permet de construire des composants sûrs à partir des exigences globales du système en interposant des spécifications abstraites et partielles entre les besoins du système et les composants eux-mêmes. Informellement, un contrat modélise le comportement abstrait d'un composant du point de vue de l'exigence à satisfaire (c. A. D garantie) dans un contexte donné (c. A. D. Hypothèse). Les contrats peuvent être exploités pour décomposer et tracer les exigences au cours d'un développement itératif, mais aussi pour effectuer une vérification compositionnelle de la satisfaction des exigences. Dans cette thèse, nous présentons une méthodologie de raisonnement à base de contrats pour la conception et la vérification de systèmes sûrs développés en SysML. Ainsi, nous définissons en UML/SysML la syntaxe des contrats et des relations de raffinement entre contrats et/ou composants qui sont utilisées pour prouver la correction du système par rapport aux exigences. Ensuite, nous proposons un cadre formel qui modélise la sémantique d'un modèle UML/SysML étendu par des contrats selon une variante d'automates temporisés entrée/sortie et nous définissons la correspondance entre ces concepts. Nous formalisons les relations de raffinement par la relation d'inclusion de traces et nous prouvons leurs propriétés compositionnelles ce qui assure la correction de la méthodologie. L'approche est instanciée pour le profil OMEGA et la boîte à outils IFx2 qui génère partiellement les obligations de preuve. Finalement, plusieurs études de cas dont une issue de l'industrie complètent la théorie pour évaluer l'approche à base de contrats et ses résultats et les comparer aux méthodes classiques de model-checkingNowadays computer systems grow larger in size and more complex. Embedded in devices from different domains like avionics, aeronautics, consumer electronics, etc. , they are often considered critical with respect to human life, costs and environment. A development that results in safe and reliable critical real-time embedded systems is a challenging task, considering that errors are accidentally inserted in the design. A way for system designers to tackle this issue is to use a compositional design technique based on components and driven by requirements: it allows to infer from global requirements, component properties that must locally hold. Contract-based reasoning allows to compositionally derive correct components from global system requirements by interposing abstract and partial specifications for components. Informally, a contract models the abstract behavior a component exhibits from the point of view of the requirement to be satisfied (i. E. Guarantee) in a given context (i. E. Assumption). Contracts can be used to decompose and trace requirements during iterative design, but also to perform compositional verification of requirement satisfaction. In this thesis, we present a methodology for reasoning with contracts during system design and verification within SysML. Thus, we define the syntax for contracts in UML/SysML, as well as a set of refinement relations between contracts and/or components in order to prove the system's correctness with respect to requirements. Next, we provide a formal framework that models the semantics of a UML/SysML model extended with contracts as a mapping of the language concepts to a variant of Timed Input/Output Automata. The refinement relations are formalized based on the trace inclusion relation and compositional properties are proved to hold which ensures the soundness of the methodology. The approach is instantiated for the OMEGA Profile and IFx2 toolset with partial automatic generation of proof obligations. Finally, the approach is applied on several case studies, including an industry-grade system model, which show its efficiency by comparative verification results
32
Daubignard, Marion. "Formalisation de preuves de sécurité concrète." Phd thesis, Université de Grenoble, 2012. http://tel.archives-ouvertes.fr/tel-00721776.
Full textAbstract:
Cette thèse se propose de remédier à l'absence de formalisme dédié aux preuves de sécurité concrète à travers 3 contributions. Nous présentons d'abord la logique CIL (Computational Indistinguishability Logic), qui permet de raisonner sur les systèmes cryptographiques. Elle contient un petit nombre de règles qui correspondent aux raisonnements souvent utilisés dans les preuves. Leur formalisation est basée sur des outils classiques comme les contextes ou les bisimulations. Deuxièmement, pour plus d'automatisation des preuves, nous avons conçu une logique de Hoare dédiée aux chiffrement asymétrique dans le modèle de l'oracle aléatoire. Elle est appliquée avec succès sur des exemples de schémas existants. Enfin, nous proposons un théorème générique de réduction pour la preuve d'indifférentiabilité d'un oracle aléatoire de fonctions de hachage cryptographiques. La preuve du théorème, formalisée en CIL, en démontre l'applicabilité. Les exemples de Keccak et Chop-Merkle-Damgard illustrent ce résultat.
33
De, Champs Thibault. "Approche à base de vérification formelle de modèle pour une utilisation sécuritaire de la cuisinière d'un habitat intelligent." Mémoire, Université de Sherbrooke, 2012. http://hdl.handle.net/11143/5774.
Full textAbstract:
Pour s'assurer que les personnes âgées soient en sécurité au domicile, le projet INOVUS s'intéresse aux risques liés à l'utilisation de la cuisinière. Dans le cadre de ce projet, les travaux de M.Sc. présentés dans ce mémoire se concentrent sur la perspective logicielle de la détection et de la prévention des risques physiques pour la personne, lors de la réalisation de tâches utilisant la cuisinière. Dans un premier temps, une revue des risques à domicile recensés dans la littérature a permis de définir la couverture nécessaire à une telle solution. Certaines situations dangereuses ont ensuite été sélectionnées pour définir un modèle de solution satisfaisant. Le développement d'une solution de sécurité pour la personne entraîne des contraintes de fiabilité de très haut niveau pour la technologie produite.Pour répondre à ce besoin, la proposition de ces travaux de M.Sc. est l'utilisation de spécifications formelles. Ces outils permettent d'obtenir un plus haut degré de fiabilité de logiciels. En se basant sur ces outils, un modèle de solution a été élaboré pour le projet INOVUS, et ce à l'aide du vérificateur de modèle ALLOY. Enfin, une implémentation en Java de ce prototype a été réalisée afin d'évaluer les résultats de détection des situations dangereuses. Ce prototype permet alors à la fois de valider l'approche de développement choisie, ainsi que d'établir une preuve de concept d'une telle solution de sécurité.
34
Luong, Hong-Viet. "Construction Incrémentale de Spécifications de Systèmes Critiques intégrant des Procédures de Vérification." Phd thesis, Université Paul Sabatier - Toulouse III, 2010. http://tel.archives-ouvertes.fr/tel-00527631.
Full textAbstract:
Cette thèse porte sur l'aide à la construction de machines d'états UML de systèmes réactifs. Elle vise à définir un cadre théorique et pragmatique pour mettre en oeuvre une approche incrémentale caractérisée par une succession de phases de construction, évaluation et correction de modèles. Ce cadre offre des moyens de vérifier si un nouveau modèle est conforme à ceux définis durant les étapes précédentes sans avoir à demander une description explicite des propriétés à vérifier. Afin de pouvoir analyser les machines d'états, nous leur associons une sémantique LTS ce qui nous a conduit à définir une procédure de transformation automatique de machines d'états en LTS. Dans un premier temps, nous avons défini et implanté des techniques de vérification de relations de conformité de LTS (red, ext, conf, et confrestr). Dans un second temps, nous nous sommes intéressés à la définition d'un cadre de construction incrémentale dans lequel plusieurs stratégies de développement peuvent être mises en \oe uvre en s'assurant que le modèle final élaboré sera une implantation conforme à la spécification initiale. Ces stratégies reposent sur des combinaisons de raffinements qui peuvent être de deux types : le raffinement vertical pour éliminer l'indéterminisme et ajouter des détails ; le raffinement horizontal pour ajouter de nouvelles fonctionnalités sans ajouter d'indéterminisme. Enfin, nous transposons la problématique de construction incrémentale d'une machine d'états à la construction d'architectures dont les composants sont des machines d'états. Des conditions sont définies pour assurer la conformité entre des architectures dans le cas de la substitution de composants.
35
Colange, Maximilien. "Symmetry reduction and symbolic data structures for model-checking of distributed systems." Paris 6, 2013. http://www.theses.fr/2013PA066724.
Full textAbstract:
Les systèmes répartis deviennent omniprésents au quotidien, en particulier dans des domaines critiques, requérant une forte garantie de fiabilité. Les approches basées sur le test sont intrinsèquement non-exhaustives, rendant nécessaire l’usage de méthodes formelles. Parmi elles, nous nous concentrons sur le model-checking, qui explore tous les comportements d’un système pour s’assurer que sa spécification est respectée. Mais cette approche se heurte à l’explosion combinatoire : le nombre d’états d’un système réparticroît exponentiellement avec son nombre de composants. Nous retenons deux des nombreuses solutions à ce problème :- les symétries pour identifier des comportements similaires : ils partagent des propriétés communes, ce qui réduit le nombre d’états à explorer. - des structures de données compactes, comme les diagrammes de décision (DD), pour réduire l’empreinte mémoire de l’exploration. Nous proposons trois principales contributions :- La réduction par symétries et les DD sont théoriquement orthogonaux, mais se combinent mal en pratique, car l’efficacité des DD repose sur l’emploi d’algorithmes dédiés. Nous proposons un nouvel algorithme pour appliquer la réduction par symétries sur des DD, et démontrons son efficacité pratique. - Classiquement, les opérations sur les DD sont encodées après un pré-calcul de toutes les entrées possibles. Nous offrons un nouveau mécanisme de manipulation des DD, entièrement symbolique, qui évite un tel pré-calcul. Nous démontrons son efficacité pour encoder une relation de transition. - Nous montrons comment ces deux contributions peuvent être appliquées à un formalisme déjà existant, les Symmetric Nets with BagsDistributed systems are becoming omnipresent in our daily life, especially in critical domains, thus requiring a strong guarantee of reliability. Approaches like testing are inherently not exhaustive, so that formal methods are needed. Among those, we focus on model-checking, that consists in exploring exhaustively all the behaviors of a system to ensure that the specification is enforced. However, this approach faces the “combinatorial explosion” problem: the number behaviors of a distributed system increases exponentially with its number of components. To tackle this explosion, several approaches have been proposed. We focus on two of them:- symmetries to identify similar behaviors: they share similar properties, thus allowing to reduce the number of behaviors to explore;- symbolic compact data structures, namely decision diagrams (DD), to reduce the memory footprint of the explored behaviors. We propose three main contributions:- Symmetry reduction and DD are theoretically orthogonal techniques, but are not known to combine well in practice, because efficiency of DD heavily relies on the use of dedicated algorithms. We propose a novel algorithm to use symmetry reduction on DD, and demonstrate experimentally its efficiency. - Classical operations on DD are encoded using a pre-computation of all possible inputs. We offer a new mechanism of manipulation of DD, fully symbolic, that avoids such a pre-computation. We demonstrate its efficiency to encode a transition relation, and to improve our symmetry reduction algorithm- We show how to use the two previous contributions to model-check an existing class of models, the Symmetric Nets with Bags
36
Xie, Yuchen. "Modélisation et Vérification Formelles de Systèmes de Contrôle de Trains." Thesis, Ecole centrale de Lille, 2019. http://www.theses.fr/2019ECLI0001.
Full textAbstract:
Le degré d'automatisation des systèmes de contrôle ferroviaire est en constante augmentation. Les industriels ferroviaires ont besoin d'un niveau accru de sécurité et de fiabilité pour remplacer les conducteurs par des systèmes de contrôle automatique des trains (ATC). Cependant, la complexité du système est également fortement augmentée par l'intégration des fonctions automatiques, ce qui rend difficile l'analyse de ces systèmes.Différentes méthodes de modélisation peuvent être utilisées pour construire les modèles du système au niveau d'abstraction approprié. Les méthodes de modélisation formelles et les méthodes de vérification formelles fournissent un cadre crucial pour assurer les propriétés de sécurité et de fiabilité. Les Réseaux de Petri constituent un outil formel approprié à la modélisation et à la vérification de systèmes critiques comme les systèmes de contrôle automatique du ferroviaire. Dans cette thèse, nous utilisons plus particulièrement les réseaux de Pétri colorés (CPNs) de Jensen pour exploiter la modularité et la hiérarchisation pour la modélisation et la vérification d’un système de grande tailleThe automation degree of railway control systems is constantly increasing. Railway industry needs the enhanced level of safety and reliability guarantee to replace the drivers by Automatic Train Control (ATC) systems. However, the system complexity is also heavily increased by the integration of automatic functions, which has caused the difficulty to analyze these systems.Different modeling methods can be used to build the system models at the appropriate level of abstraction. Formal modeling methods and formal verification methods can provide crucial support to ensure safety and reliability properties. Petri Nets are a suitable tool for modeling and verifying critical systems such as automatic train control systems. In this thesis, we use more specifically Colored Petri Nets (CPNs) to exploit modularity and hierarchization for the modeling and verification of a large-scale system
37
Boulanger, Jean-Louis. "Expression et validation des propriétés de sécurité logique et physique pour les systèmes informatiques critiques." Compiègne, 2006. http://www.theses.fr/2006COMP1622.
Full textAbstract:
Dans le cadre de nos activités de recherche, nous nous sommes intéressés à la mise en sécurité des systèmes dits critiques (pouvant en cas de défaillance causer des dommages sérieux aux personnes ou aux biens). La mise en sécurité de tels systèmes passe par l'expression de recommandations liées à la sécurité. Ces recommandations peuvent provenir d'une demande du client (clauses du cahier des charges), de l'état de l'art, d'un référentiel légal (normes, décrets, arrêtés,. . ) ou d'études sur les conséquences des défaillances du système sur l'environnement, les personnes, l'image de marque de l'entreprise, etc. À partir des recommandations introduites dans le cahier des charges du client, il est donc possible d'identifier des "exigences". Il faudra alors démontrer que ces exigences sont prises en compte sur l'ensemble du cycle de réalisation du système. Dans le cadre de cette thèse, nous proposons une méthode et des exemples de mise en œuvre qui se basent sur l'identification, l'expression et la vérification des exigences liées à la sécuritéWithin the framework of our research activities, we were interested in the safety of critical systems (whose failure can cause serious damage to people, goods or environment). The design of the safety of such systems requires the expression of safety-related recommendations. These recommendations can come from requirements of the customer (contractual clauses), from the state of the art, from legal reference frame (standards, decrees, laws) or from studies of the consequences of the failures on the system, the people, the environment. Starting from the safety recommendations coming from contractual conditions of the customer, it is thus possible to identify "safety requirements". It will have then to be proved that these safety requirements are taken into account during the whole design and lifecycle of the system. Within the framework of this thesis, we propose a method and implementation examples, which are based on the identification, the expression and the verification of the safety requirements
38
Hördegen, Heinrich. "Vérification des protocoles cryptographiques : comparaison des modèles symboliques avec une application des résultats : étude des protocoles récursifs." Thesis, Nancy 1, 2007. http://www.theses.fr/2007NAN10083.
Full textAbstract:
Cette thèse traite de la vérification des protocoles cryptographiques. Son sujet est la modélisation symbolique de protocoles avec pour objectif la preuve de propriétés de sécurité. La thèse comprend deux parties: La première partie définit quatre modèles symboliques différant par les moyens syntaxiques que les concepteur peuvent utiliser pour représenter les primitives cryptographiques. On a observé que les vérificateurs utilisent des astuces de codage dans des modèles peu riches pour représenter les primitives manquantes. Nous montrons que ces codages sont corrects dans le sens où un protocole qui satisfait une propriété dans un modèle peu expressif la satisfait aussi dans un modèle plus riche. Nous terminons cette partie par la description d'un module que nous avons implémenté pour la plate-forme de vérification AVISPA. Ce module est basé sur des résultats permettant le transfert des propriétés d'un protocole, prouvées dans un modèle symbolique, vers un modèle calculatoire. Dans la deuxième partie de cette thèse, nous développons un modèle symbolique pour représenter des protocoles récursifs. Ces protocoles sont difficiles à analyser et peu de résultats de décidabilité existent. Nous montrons que notre modèle symbolique permet de retrouver une attaque connue contre une propriété d'un protocole de commerce électronique. Nous proposons ensuite une modification de ce protocole et montrons que le protocole modifié satisfait cette propriétéThis thesis deals with formal verification of cryptographic protocols. It is about symbolic modelling of protocols with the objective to prove security properties. The thesis is split in two parts: The first part defines four symbolic models which differ in the syntactic resources that protocol designers may use do model cryptographic primitives. We found that engineers employ coding dodges in order to model missing cryptographic primitives in simpler models. We showed that these codings are correct in that protocol properties that are proven in lean models also hold in more elaborated models. We finish this part with the description of a module implementation for the verification plate-form AVISPA. The module is based on results that allow to automatically translate protocol properties, proven in symbolic models, to computational models. In the second part of this thesis, we develop a symbolic model in order to represent ecursive protocols. This class of protocols is difficult to analyse and, so far, there are only few decidability results. We show that our symbolic model allows us to retrieve an previously known attack against a special security property of an e-commerce protocol. We then modify this protocol and show that the property holds for the modified protocol
39
Evrot, Dominique. "Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle." Phd thesis, Université Henri Poincaré - Nancy I, 2008. http://tel.archives-ouvertes.fr/tel-00344890.
Full textAbstract:
L'introduction des nouvelles technologies de l'information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu'ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d'un réseau d'interactions entre ces constituants qui peut être à l'origine de comportements néfastes et difficiles à prévoir. Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées " système ", qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s'assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences " système " formulées par les utilisateurs.
Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l'identification, la formalisation et la structuration d'exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d'une part, sur un raffinement prouvé (par theroem proving) des exigences " système " permettant d'établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d'autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques.
40
Roux, Mattias. "Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories." Thesis, Université Paris-Saclay (ComUE), 2019. http://www.theses.fr/2019SACLS582.
Full textAbstract:
Cette thèse se propose de présenter plusieurs extensions ayant été ajoutées au vérificateur de modèles Cubicle.Cubicle est un logiciel permettant de vérifier automatiquement la sûreté de systèmes paramétrés au moyen de techniques de vérification de modèles modulo théories.La première contribution apportée par cette thèse consiste en l'implémentation d'un nouvel algorithme d'atteignabilité baptisé FAR (pour Forward Abstracted Reachabilty). FAR est un algorithme faisant intervenir à la fois des techniques de l'analyse d'atteignabilité en arrière déjà implémentée dans Cubicle ainsi que des techniques d'analyse d'atteignabilité en avant.La seconde contribution est constituée de multiples ajouts inspirés de méthodes de l'intelligence artificielle afin d'améliorer la génération automatique d'invariants de Cubicle.Enfin, la dernière contribution a permis d'augmenter l'expressivité de Cubicle afin de prouver des propriétés faisant intervenir des quantificateurs universels. Cette contribution a été mise en œuvre en associant Cubicle à Why3, une plateforme de vérification déductiveThis thesis proposes to present several extensions that have been added to the Cubicle model checker.Cubicle is a software allowing to automatically check the safety of parameterized systems using model checking modulo theory techniques.The first contribution made by this thesis consists in the implementation of a new reachability algorithm called FAR (for Forward Abstracted Reachabilty). FAR is an algorithm involving both backward reachability analysis techniques already implemented in Cubicle as well as forward reachability analysis techniques.The second contribution consists of multiple additions inspired by artificial intelligence methods to improve the automatic generation of Cubicle invariants.Finally, the last contribution has increased Cubicle's expressiveness in order to prove properties involving universal quantifiers. This contribution was implemented by associating Cubicle with Why3, a deductive verification platform
41
Vandermeulen, Eric. "La Machine Séquentielle Interprétée : un modèle à états pour la représentation discrète et la vérification de systèmes." Montpellier 2, 1996. http://www.theses.fr/1996MON20070.
Full textAbstract:
Nous definissons le modele de machine sequentielle interpretee msi. Ce modele, a etats, synchrone, est enrichi par l'introduction de donnees et d'operations, ce qui permet de decrire aussi bien le comportement du systeme que ses interactions avec son environnement. Une representation de ce modele a l'aide d'une logique temporelle permet alors d'y associer des outils de verification formelle. Pour illustrer l'utilisation du modele de msi, et les mecanismes de preuve associes, nous decrivons la commande d'un organe de pilotage d'un systeme automatise de production: le projet korso. Nous pouvons ainsi verifier diverses proprietes
42
Ouenzar, Mohammed. "Validation de spécifications de systèmes d'information avec Alloy." Mémoire, Université de Sherbrooke, 2013. http://hdl.handle.net/11143/6594.
Full textAbstract:
Le présent mémoire propose une investigation approfondie de l’analyseur Alloy afin de juger son adaptabilité en tant que vérificateur de modèles. Dans un premier temps, l’étude dresse un tableau comparatif de six vérificateurs de modèles, incluant Alloy, afin de déterminer lequel d’entre eux est le plus apte à résoudre les problématiques de sécurité fonctionnelle posées par les systèmes d’information. En conclusion de cette première phase, Alloy émerge comme l’un des analyseurs les plus performants pour vérifier les modèles sur lesquels se fondent les systèmes d’information. Dans un second temps, et sur la base des problématiques rencontrées au cours de cette première phase, l’étude rapporte une série d’idiomes pour, d’une part, présenter une manière optimisée de spécifier des traces et, d’autre part, trouver des recours afin de contourner les limitations imposées par Alloy. À ces fins, le mémoire propose deux nouveaux cas d’espèce, ceux d’une cuisinière intelligente et d’une boîte noire, afin de déterminer si oui ou non l’analyseur est capable de gérer les systèmes dynamiques possédant de nombreuses entités avec autant d’efficacité que les systèmes qui en possèdent moins. En conclusion, le mémoire rapporte que Alloy est un bon outil pour vérifier des systèmes dynamiques mais que sa version récente, DynAlloy, peut être encore mieux adapté pour le faire puisque précisément conçu pour faire face aux spécificités de ce type de système. Le mémoire s’achève sur une présentation sommaire de ce dernier outil.
43
Sahli, Nabil. "Contribution au problème de la sécurité sémantique des systèmes : approche basée sur l'ingénierie dirigée par les modèles." Electronic Thesis or Diss., Aix-Marseille, 2019. http://www.theses.fr/2019AIXM0699.
Full textAbstract:
Les infrastructures industrielles critiques seront dotées de plusieurs équipements embarqués intelligents. Elles exploitent des systèmes complexes, embarqués, intelligents et sémantiques pour leurs fonctionnements, en local et à distance, dans un contexte de développement, de villes intelligentes et du web des objets. Elles emploient, de plus en plus de systèmes «contrôle/commande», pour la surveillance des plateformes industrielles critiques, en temps réel. Les infrastructures critiques seront de plus en plus communicantes dans le cadre des échanges des alarmes et la mise en place de marchés euro-méditerranéens de l’électricité et davantage plus vulnérables. La cybernétique des plateformes critiques se développe, de jour en jour, essentiellement avec l’usage de systèmes complexes embarqués intelligents sémantiques, des services web, des ontologies,..etc. Ils sont tous embarqués sur les instruments intelligents, composant les systèmes sémantiques. Des réseaux de télécommunication intelligents, filaire et sans fil, dit hybrides, se développent. Ils représentent un grand challenge, pour la sécurité des systèmes communicants futurs. Dans un contexte de développement du web, des objets et des villes intelligentes, nos travaux de recherche visent à renforcer les bases de la sécurité et de la cybernétique sémantique, pour les systèmes communicants. Dans notre solution globale, en matière de sécurité sémantique, des infrastructures critiques, nous avons proposé plusieurs sous-solutions, tels que des méta-modèles et des modèles, ainsi qu’une stratégie de sécurité de bout en bout, avec un fonctionnement sur un réseau Cloud global, hybride et sécuriséCritical, modern, current, and even future industrial infrastructures will be equipped with several intelligent embedded equipment. They exploit complex, embedded, intelligent and semantic systems for their operations, locally and remotely, in a context of development, smart cities and the web of things. They are using more and more SCADA and DCS control systems to monitor critical industrial platforms in real time. Critical infrastructures will be more and more communicating in the framework of the exchanges of allarmes and the establishment of Euro-Mediterranean markets of the életcricité and also more and more vulnerable, to classic and even semantic attacks, to viruses, to Trojan horses. The cybernetics of critical platforms is growing, day by day, mainly with the use of complex embedded intelligent semantic systems, web services, ontologies, and format files (XML, OWL, RDF, etc.). They are all embedded in intelligent instruments, making up semantic SCADA systems. Intelligent telecommunication networks, wired and wireless, called hybrids, are developing. They represent a great challenge for the security of future communicating systems. In a context of development of the web of things and smart cities, our research aims to strengthen the bases of security and semantic cybernetics, for communicating systems. In our global solution for semantic security, critical infrastructures, we have proposed several sub-solutions, such as metamodels and models, as well as an end-to-end security strategy, with operation on a global cloud network, hybrid and secure
44
Christofi, Maria. "Preuves de sécurité outillées d’implémentations cryptographiques." Versailles-St Quentin en Yvelines, 2013. http://www.theses.fr/2013VERS0029.
Full textAbstract:
Dans cette thèse, nous nous sommes intéressés à la vérification formelle des implémentations cryptographiques. Dans la première partie, nous étudions la vérification du protocole mERA à l’aide d’outil ProVerif. Nous vérifions que ce protocole assure certaines propriétés de sécurité, notamment l’authentification, le secret et la non-reliabilité, ainsi que des propriétés comme la vivacité du protocole. Dans la deuxième partie de cette thèse, nous étudions la vérification formelle des implémentations cryptographiques vis-à-vis d’un certain type d’attaque: les attaques par injection de faute modifiant les données. Nous identifions et présentons les différents modèles de ce type d’attaque en tenant en compte plusieurs paramètres. Ensuite, nous modélisons des implémentations cryptographiques (munies de contremesures), nous injectons tous les scenarios de fautes possibles et finalement nous vérifions le code correspondant à l’aide d’outil Frama-C, basé sur l’analyse statique. Nous présentons une application de notre méthode : la vérification d’une implémentation RSA-CRT munie de la contremesure de Vigilant (CHES 2008). Après avoir exprimé les propriétés nécessaires pour la vérification, nous injectons tous les scenarios de fautes possibles (en tenant compte d’un modèle de faute choisi). Cette vérification révèle deux scenarios de fautes provoquant deux attaques susceptibles à fuir des informations secrètes. Afin de mécaniser la vérification, nous avons réussi à automatiser complètement l’insertion des fautes selon les différents modèles (en tenant en compte les attaques mono-fautes, ainsi que les multi-fautes). Ceci a donné naissance à un nouveau plug-in de Frama-C : TL_FACEIn this thesis, we are interested on the formal verification of cryptographic implementations. In the first part, we study the verification of the protocol mERA using the tool ProVerif. We prove that this protocol verifies some security properties, like the authentication, the secrecy and the unlinkability, but also properties like its vivacity. In the second part of this thesis, we study the formal verification of cryptographic implementations against an attack family: attacks with fault injection modifying data. We identify and present the different models of these attacks considering different parameters. We then model the cryptographic implementation (with its countermeasures), we inject all possible fault scenarios and finally we verify the corresponding code using the Frama-C tool, based on static analysis techniques. We present a use case of our method: the verification of an CRT-RSA implementation with Vigilant’s countermeasure. After expressing the necessary properties for the verification, we inject all fault scenarios (regarding the chosen fault model). This verification reveals two fault scenarios susceptible to flow secret information. In order to mechanize the verification, we insert fault scenarios automatically according to both single and multi fault attacks). This creates a new Frama-C plug-in: TL-FACE
45
Tigori, Kabland Toussaint Gautier. "Méthode de génération d’exécutif temps-réel." Thesis, Ecole centrale de Nantes, 2016. http://www.theses.fr/2016ECDN0019.
Full textAbstract:
Dans les systèmes embarqués, la spécialisation ou la configuration des systèmes d’exploitation temps réel en fonction des besoins de l’application consiste en la suppression des services inutiles du système d’exploitation. Cela a non seulement pour but d’optimiser l’empreinte mémoire occupée par le système d’exploitation temps réel, afin de satisfaire les contraintes de mémoire auxquelles les systèmes embarqués font face, mais aussi de réduire la quantité de code mort au sein du système d’exploitation temps réel afin d’améliorer la sureté de fonctionnement. Dans nos travaux de thèse, nous nous intéressons à l’utilisation des méthodes formelles dans le processus de spécialisation des systèmes d’exploitation temps réel. Une difficulté majeure dans l’utilisation de modèles formels est la distance entre le modèle et le système modélisé. Nous proposons donc de modéliser le système d’exploitation de telle sorte que le modèle embarque son code source et les structures de données manipulées. Nous utilisons à cet effet un modèle à états finis (éventuellement temporisé) augmenté par des variables discrètes et des séquences d’instructions, considérées comme atomiques, manipulant ces variables. À partir du modèle du système d’exploitation et d’un modèle de l’application visée, l’ensemble des états accessibles du modèle du système d’exploitation traduisant le code effectivement utilisé lors de l’exécution de l’application est calculé. Le code source du système d’exploitation spécialisé est extrait de ce modèle élagué. L’ensemble de la démarche exposée est mise en oeuvre avec Trampoline, un système d’exploitation temps réel basée sur les standards OSEK/VDX et AUTOSAR. Cette technique de spécialisation garantit l’absence de code mort, minimise l’empreinte mémoire et fournit un modèle formel du système d’exploitation utilisable dans une étape ultérieure de modelchecking. Dans ce cadre, nous proposons une technique automatique de vérification formelle de la conformité aux standards OSEK/VDX et AUTOSAR à l’aide d’observateurs génériquesIn embedded systems, specialization or configuration of real-time operating systems according to the application requirements consists to remove the operating system services that are not needed by the application. This operation allows both to optimize the memory footprint occupied by the real-time operating system in order to meet the memory constraints in embedded systems and to reduce the amount of dead code inside the real-time operating system in order to improve its reliability. In this thesis, we focus on the use of formal methods to specialize real-time operating systems according applications. One major difficulty using formal models is the gap between the system model and its implementation. Thus, we propose to model the operating system so that the model embeds its source code and manipulated data structures. For this purpose, we use finite state model (possibly timed model) with discrete variables and sequences of instructions which are considered as atomic manipulating these variables. From the operating system model and an application model, the set of reachable states of the operating system model describing the code needed during application execution is computed. Thus, the source code of the specialized operating system is extracted from the pruned model. The overall approach is implemented with Trampoline, a real-time operating system based on OSEK/VDX and AUTOSAR standards. This specialization technique ensures the absence of dead code, minimizes the memory footprint and provides a formal model of the operating system used in a last step to check its behavior by using model checking. In this context, we propose an automatic formal verification technique that allows to check the operating systems according OSEK/VDX and AUTOSAR standards using generic observers
46
Gazagnaire, Thomas. "Langages de scénarios : Utiliser des ordres partiels pour modéliser, vérifier et superviser des systèmes parallèles et répartis." Phd thesis, Université Rennes 1, 2008. http://tel.archives-ouvertes.fr/tel-00322528.
Full textAbstract:
Cette thèse se place dans le cadre de la modélisation et de l'analyse de systèmes parallèles et répartis. Plus précisément, nous nous intéressons à la modélisation, la vérification et la supervision de systèmes, composés d'entités indépendantes interagissant localement par mémoire partagée et globalement par échange asynchrone de messages.Dans ce contexte, plutôt que de modéliser séparément chaque entité, puis d'analyser les comportements qui peuvent se produire lorsque ces entités interagissent, nous fournissons une théorie permettant de modéliser globalement le système considéré tout en conservant des propriétés de vérification et de supervision décidables. Cette théorie se base sur le formalisme des ordres partiels étiquetés (appelés "pomsets").
Dans ce but, nous définissons le modèle des HMSC causaux qui étend le formalisme des HMSC en autorisant, comme pour les traces de Mazurkiewicz, certains événements à commuter sur chaque processus. Nous montrons, tout d'abord, qu'une restriction syntaxique des HMSC causaux a le même pouvoir d'expression que les réseaux bornés d'automates mixtes, un modèle qui étend les réseaux d'automates asynchrones de Zielonka et les réseaux d'automates communicants. De plus, nous montrons que les méthodes classiques de model-checking de systèmes séquentiels peuvent s'appliquer aux modèles plus concis basés sur les pomsets, comme les HMSC causaux, sans perte d'efficacité. Enfin, nous proposons des méthodes de traitement efficace d'observations volumineuses d'exécutions réparties, ainsi que des techniques de supervision, telles que le diagnostic ou la corrélation d'événements, qui utilisent des modèles basés sur les pomsets.
47
Le, Cornec Yves-Stan. "Analyse de systèmes modulaires à l'aide de techniques d'abstractions hiérarchiques." Thesis, Université Paris-Saclay (ComUE), 2016. http://www.theses.fr/2016SACLE019/document.
Full textAbstract:
Dans cette thèse, on s’intéresse au problème de l’explosion combinatoire du model-checking sur des systèmes modulaires. Les techniques d’abstractions hiérarchiques permettent de construire de manière incrémentale une abstraction d’un modèle en composant des abstractions de ses parties. Cette opération doit en outre préserver les propriétés d’intérêt du modèle.Dans un premier temps, on définit le formalisme des réseaux de régulation modulaires, dans le but de pouvoir étudier des systèmes biologiques en utilisant de l’abstraction hiérarchique. On utilise ensuite cette méthode pour détecter les états stables accessibles depuis un état donné sur un modèle multicellulaire intervenant lors du développement embryonnaire de la drosophile. L’opération d’abstraction SAFETY utilisée préserve l’accessibilité de tous les états stable. C’est une réduction classique et générique dans le sens ou elle préserve également toutes les propriétés de sûreté d’un système. Dans un second temps, on suppose que l’on a connaissance de la formule globale (exprimée en μ-calcul) que l’on veut vérifier, ainsi que de l’état initial du module. On défini alors deux opérations de réduction différentes. Ces réductions ont pour seule contrainte de préserver la valeur global de la formule et il est donc possible d’obtenir des réductions plus importantes qu’avec les méthodes génériques (le but reste le même : réduire la taille d’un module ou d’un sous-système donné sans avoir connaissance du reste du système). Lors du calcul de cette réduction, on effectue de l’analyse partielle pour déterminer si le sous-système contient assez d’information pour connaître la valeur de vérité de la for-mule sur le système global. Si c’est le cas, on peut arrêter là l’analyse par abstraction hiérarchique ; sinon, cette étape est tout de même utile pour réduire le module.Enfin, on teste la première de ces réductions à l’aide d’un prototype sur quelques exemples simples. En plus de constater les coefficients de réduction obtenus, cela permet de fournir des données pour s’attaquer par la suite au problème du meilleur ordre d’analyse hiérarchique. C’est en effet un problème difficile et l’ordre d’analyse a une grande influence sur les performances de ces méthodesIn this thesis, we are interested in limiting the combinatorial explosion that happens when model-checking modular systems. We use hierarchical abstraction techniques, which allow one to build an abstraction of a modular system by composing abstractions of his part, while ensuring that this abstraction does not change the temporal properties we are interested in. At first, we define the modular regulation networks formalism in or-der to apply hierarchical abstraction techniques to the study of biological systems. We then use this approach to find the reachable stable states of a multi-cellular model involved in the development of the fruit fly embryo. For this, we use the abstraction called SAFETY which reduces a system while keeping all of its reachable stable states. This is a classical reduction which is quite general in the sens that it also preserves all the safety properties of the model. After this, we define two new reduction operations, which are dependent on the μ-calculus formula we seek to verify on the global system. We also assume that we know the initial state of the module or sub-system to be reduced. Since these reductions must only preserve the value of one formula over the global system, they should be able to return smaller systems than the general ones. While computing these reductions on one module or sub-system, we use partial analysis techniques to test if it contains enough information to conclude about the truth value of the formula on the global system. If it is the case, we can stop the incremental analysis right away ; otherwise, this step is still useful for the computation of the reduced sub-system. Finally, we use a prototype to test the first one of our reduction operations on some simple examples. This enables us to observe how big the reductions are as well as getting data in order to tackle the problem of the order of analysis in the future. It is a difficult question and an important one since the hierarchical order in which we build the abstraction has a huge weight on the efficiency of these methods
48
Ngo, Van Chan. "Vérification Formelle d'un Compilateur Synchrone: de Signal vers C." Phd thesis, Université Rennes 1, 2014. http://tel.archives-ouvertes.fr/tel-01058041.
Full textAbstract:
Les langages synchrones tels que SIGNAL, LUSTRE et ESTEREL sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de SIGNAL. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé.
49
Akhtar, Nadeem. "Contribution à la spécification formelle et à la vérification de systèmes multi-agents robotiques." Lorient, 2010. http://www.theses.fr/2010LORIS190.
Full textAbstract:
L'une des tâches les plus difficiles en ingénierie des spécifications de systèmes multi-agents robotiques est d'assurer les propriétés d’exactitude que sont la sûreté et la vivacité. Comme ces systèmes complexes sont concurrents et s’exécutent dans des environnements dynamiques et distribués, leur spécification formelle, leur vérification ainsi que leur transformation par raffinement jouent un rôle majeur dans la fiabilité du système. Nos objectifs sont de proposer une approche de développement basée sur une combinaison de méthodes et de techniques qui permettent la vérification formelle et la validation pendant la définition des spécifications et qui soit flexible. Cette approche permet la transformation par raffinement des spécifications abstraites et des propriétés fonctionnelles et non-fonctionnelles en des spécifications concrètes permettant leur vérification formelle. Les systèmes multi-agents robotiques sont des systèmes concurrents ayant des processus parallèles qui peuvent avoir des besoins de synchronisation. Une étude de cas de systèmes multi-agents robotiques a été présentée pour illustrer des spécifications formelles et leurs vérifications. Une combinaison d'algèbre de processus et de techniques basées sur des automates à état nous a permis de défini r les spécifications formelles de notre système, vérifier les propriétés de sûreté et de vivacité ainsi que le déroulement possible d'exécutions simultanées, cela nous a également permis d’identifié les avantages des méthodes formelles pour les systèmes multi-agents robotiques. Les méthodes formelles et les langues sont fondées sur des bases mathématiques solides. Notre capacité à construire des systèmes complexes devient d’autant plus grande que les techniques de vérification formelles deviennent plus matures. Pour traiter les problèmes de complexité des systèmes multi-agent et obtenir des résultats significatifs avec l'analyse formelle, nous devons nous occuper de la complexité à chaque stade du système multi-agent : de la phase de spécification à l'analyse, conception et la phase de vérification. La vérification formelle peut accomplir la couverture exhaustive complète du système garantissant ainsi que les échecs non détectés dans le comportement sont exclus. L'approche prise est de spécifier formellement chaque sous-portion d'un système et de la vérifier et ensuite, si c'est en accord avec du système ensemble, passer à la vérification formelle de chaque sous-partie du système. De cette manière les propriétés de sûreté et de vivacité du système peuvent être prouvées en formalisant les différentes composantes et des processus dans le cycle de vie de développement de système. Avoir une fondation formelle pour les langues et les instruments permit : l’amélioration de la documentation et la compréhension des spécifications, l'analyse rigoureuse de propriétés de système, être certain que les transformations et l'implémentation sont possibles sans erreur tout en conservant leurs propriétés, l’amélioration de la rigueur et de la qualité du processus de développement entier et fournir une fondation ferme pendant le processus d'évolution et d’adaptation. Par conséquent une solution est proposée se composant des méthodes multiples et des techniques pour la spécification formelle et la vérification de ces systèmes. Nous avons utilisé la méthode multi-agents Gaia ainsi que des processus et des automates d’états finis, et avons défini les spécifications formelles de notre système, vérifié leur correction avec propriétés de sûreté et de vivacité en générant tous les flux d'exécutions possibles. La logique temporelle LTS utilise le Processus d'État Fini (FSP) comme langue de contribution pour officiellement définir et vérifier que notre système et vérifier ses limites par l'enquête exhaustive de système expose l'espace pour la vérification formelle de chaque composante du système pour garantir les propriétés de sûreté et de vivacité. π-ADL dot NET est utilisé pour définir l'architecture de système et vérifier les aspects statiques aussi bien que dynamiques d'architecture. Le système est exécuté en utilisant le Microsoft Robotics Developer Studio (MRDS) l'environnement de simulation. Cette recherche présente une étude de cas complète qui est illustré au travers de la spécification d’un système multi-agents robotiquesOne of the most challenging tasks in software engineering for multi-agent robotic systems is to ensure correctness properties of safety and liveness. As these systems have concurrency, and often have dynamic environments, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play a major role in system correctness. The problem statement is: How can a safe multi-agent robotic system be developed? Here by safe the focus is on correctness properties which can be described by a combination of safety and liveness. How can safety and liveness properties be enforced during the development of multi-agent robotic system? Our objectives are to propose a development approach based on a combination of methods and techniques that allow for formal verification and evaluation during specification definition and that is also flexible. An approach which supports analysis with respect to functional, as well as non-functional properties by step-wise refinement from abstract to concrete specifications and then formal verification of these specifications. We have analysed the development process of a robotic multi-agent system after classifying it in the major phases of requirement specifications, verification specifications, architecture specifications and implementation. Formal methods and languages are based on a solid mathematical foundation. To catch up with the complexity problems in multi-agent systems and get significant results with formal analysis, we must cope with complexity at every stage of development: from the specification phase to the analysis, design and verification phase. Formal verification can be used for exhaustive investigation of system space thus ensuring that undetected failures in the behaviour are excluded. We construct the system incrementally from subcomponents, based on software architecture. State reduction is achieved by hiding actions and minimising; property checks remain in the minimised subcomponents. Each component of a specification is described as LTS, which has all the possible states a component may reach and all possible transitions it may perform. The reasons for having a formal foundation for the languages and tools are: (1) to enable rigorous analysis of system properties; (2) to be as certain as possible that the specifications, transformations, and implementation are property-preserving and error-free; (3) to improve rigor and quality of the whole development process; (4) to provide a firm foundation during the adaptation and evolution process; (5) to improve documentation and understanding of specifications. A solution has been proposed for formal specification and verification of safety and liveness properties. Our contributions are (1) an approach based on a combination of methods to allow for formal verification and evaluation during requirement specifications, verification specifications, architecture specifications, and implementation; (2) checking safety and liveness properties of correctness during each development phase; (3) a multi-agent robotic system case study to exemplify formal specifications and verification; (4) a combination of process algebra and finite automata based techniques to define the formal specifications of our system, using a model-checking method and verifying all possible flow of concurrent executions; (5) identifying the benefits of formal methods for multi-agent robotic systems. We have used the Gaia multi-agent method for requirement specifications; Labelled Transition Systems (LTS) based finite automata techniques, which take Finite State Process (FSP) as input language for verification specification; The π-ADL dot NET is used to define architecture specifications and check the static, as well as dynamic aspects of architecture; Then the system is implemented by using Service-Oriented Architecture (SOA) based Microsoft Robotics Developer Studio (MRDS) simulation environment
50
Leroux-Beaudout, Renan. "Méthodologie de conception de systèmes de simulations en entreprise étendue, basée sur l'ingénierie système dirigée par les modèles." Thesis, Toulouse 3, 2020. http://www.theses.fr/2020TOU30089.
Full textAbstract:
Ce manuscrit présente une méthodologie pour la conception de systèmes de simulation de modèles en entreprise étendue, basée sur l'ingénierie système dirigée par les modèles. Le but est de permettre à l'architecte système d'explorer des solutions alternatives et de vérifier et/ou valider l'architecture du système en cours de conception, en regard des exigences et besoins des parties prenantes. Cette méthodologie se décline suivant deux axes complémentaires : la partie méthode et les moyens d'exécution, sans lesquels il ne peut y avoir de simulation. Cette nouvelle méthode se fonde sur le principe suivant : partir des exigences utilisateur pour créer les modèles d'architecture système, puis en dériver l'architecture de simulation, développer les modèles exécutables et exécuter la simulation en relation avec les objectifs de vérification et/ou validation. En agissant ainsi, les écarts d'interprétations potentiels entre le modèle d'architecture système et les modèles de simulation sont supprimés ou à tout le moins réduits, par rapport à une approche traditionnelle. Cette nouvelle méthode est de type matriciel. Les colonnes représentent les acteurs, tandis que les lignes correspondent aux différentes étapes de la méthode MBSE employée par l'architecte système pour le produit, y compris les étapes de raffinements. Les acteurs sont l'architecte système pour le produit (SyA), un premier nouvel acteur introduit par cette méthode : l'architecte système pour la simulation (SiA), les développeurs des modèles exécutables de simulation (SMD). Un second nouvel acteur est en charge de l'exécution de la simulation (SEM) au sein de chacune des entreprises, en charge de l'analyse et de la production des résultats exploitables par l'architecte système pour le produit. Avec cette méthode matricielle, le SyA peut demander des simulations, soit en profondeur pour préciser un point particulier de son modèle, soit en extension pour vérifier la bonne concordance des fonctions entre elles, tout en réutilisant des fonctions déjà définies durant les étapes amont ou aval de ses décompositions précédentes. Au global, gains de temps, de coûts, et de confiance. Le deuxième axe de cette méthodologie concerne la réalisation d'une plateforme de cosimulation en entreprise étendue (EE), qui est un projet en soi. Le MBSE a permis de définir une architecture fonctionnelle et physique de cette plateforme de cosimulation qui peut être amendée en fonction des besoins exprimés par l'architecte de la simulation. La proposition introduit un troisième nouvel acteur : le Infrastructure Project Manager (IPM) qui est en charge de la coordination pour la réalisation de la plateforme de cosimulation, au sein de son entreprise. Pour une EE de type donneur d'ordres à soustraitants, introduction de deux nouveaux acteurs : le superviseur d'IPM et le responsable de l'exécution des simulations (SEM), dont leurs rôles respectifs sont de faire le lien avec leurs pendants chez les partenairesThis manuscript presents a methodology for the design of "early" simulations in extended enterprise, based on model-driven system engineering. The goal is to allow the system architect to explore alternative solutions, and to verify and/or validate the system architecture being designed, in relation to the user requirements. This methodology is divided into two complementary axes : the method part (new) and the means of execution, without which there can be no simulation. This new method is based on the following principle : starting from the user requirements to create the system architecture model, then derive the simulation architecture, develop the executable models and run the simulation in relation to objectives of verification and/or validation. By doing this, potential differences in interpretations between the system architecture model and simulation models are removed or at least reduced compared to a traditional approach. This method is of matrix type. The columns represent the actors, while the lines correspond to the different steps of the MBSE method used by the system architect for the product, including the refinement steps. The actors are the system architect for the product (SyA), a first new actor introduced by this method : the system architect for the simulation (SiA), the developers of the simulation executable models (SMD), and the second new actor in charge of the execution of the simulation (SEM). The analysis of its qualities and the production of results exploitable by the system architect for the product. As the method relies on a matrix structure, the SyA can request simulations, either in depth to specify a particular point of its model, or more in extension to check the good agreement of the functions between them. With this new matrix approach, the system architect for the product can reuse functions already defined during the upstream or downstream stages of its previous decompositions. Overall, saving time, costs, and confidence. The second axis of this methodology is the realization of an extended enterprise cosimulation (EE) platform, which is a project in itself. Based on a proposal of requirements specifications, the MBSE has defined a functional and physical architecture. The architecture of this platform can be modified according to the simulation needs expressed by the architect of the simulation. This is one of his prerogatives. The proposal introduces a third new player : the Infrastructure Project Manager (IPM) which is in charge of coordinating for the realization of the cosimulation platform, within his company. For an EE of federated type, that is to say from contractor to subcontractor, introduction of two new actors : - the supervisor of IPM, whose rôle is to link IPMs to solve the administrative and interconnection problems, - the person responsible in charge of the execution simulations. He coordinates, with the SEM of each partner, the implementation of simulations, ensures launches, and returns the results to all partners