Spelling suggestions: "subject:"systèmes critique""
1 |
Traceability of concerns and observer-based verification for railway safety-critical software / Traçabilité des exigences et vérification par observateurs pour les logiciels critiques des systèmes ferroviairesSango, Marc 18 September 2015 (has links)
Ces dernières années, le monde des systèmes critiques a connu un véritable essor en matière de demande de logiciels. Dans une optique majeure de réduction des coûts de développement, les grands acteurs du monde critique comme ceux de l’avionique et de l’automobile s’orientent de plus en plus vers l’ingénierie dirigée par les modèles. Par contre les acteurs du domaine ferroviaire, pour des raisons stratégiques et organisationnelles restent encore fidèles à des méthodes conventionnelles qui leur permettent de tirer au maximum profit de leurs compétences. Cependant, ces approches conventionnelles souffrent d’un manque d’abstraction pour la traçabilité des préoccupations et la vérification formelle, qui sont fortement recommandées dans le développement des logiciels critiques dans le domaine ferroviaire. Pour faire face à ces limitations, nous présentons dans cette thèse une approche systématique basée sur l’ingénierie dirigée par les modèles à base de composants, de façon à maîtriser au mieux la complexité des logiciels et la traçabilité des préoccupations. Nous proposons notamment trois contributions essentielles. En premier lieu, nous fournissons un ensemble uniformisé de méta-modèles permettant de décrire les préoccupations des exigences logicielles, les composants logiciels, et la traçabilité entre les préoccupations et ces composants logiciels. Avec la deuxième contribution, nous proposons un support formel de notre modèle pour en permettre la vérification formelle. Finalement, la dernière contribution propose une approche de développement et de vérification à base de composants logiciels, nommée SARA pour "SAfety-critical RAilway control applications". Nous avons validé notre approche avec quelques cas d’études du nouveau système européen de contrôle de train, ERTMS/ETCS. / In recent years, the development of critical systems demands more and more software. In order to reduce their costs of development and verification, actors in critical domains, such as avionics and automotive domains, are moving more and more towards model-driven engineering. In contrast, in the railway domain, for strategic and organizational reasons, actors remain faithful to traditional methods that allow them to take advantage of their knowledge. However, these conventional approaches suffer from a lack of abstraction and do not provide supports for traceability of concerns and formal verification, which are highly recommended for the development of railway safety-critical software. To address these shortcomings, we present in this thesis a systematic approach based on model driven engineering and component-based model, in order to better manage software complexity and traceability of concerns. In this dissertation, we provide in particular three major contributions. First, we provide an integrated set of meta-models for describing the concerns of software requirements, software components, and traceability between the concerns and software components. With the second contribution, we propose a formal support of our model to allow formal verification of temporal properties. Finally, with the last contribution, we propose a software component-based development and verification approach, called SARA, and included in V-lifecycle widely used in the railway domain. Experiments we conducted to validate our approach through a few case studies of the new European train control system ERTMS/ETCS, show that by using component model that explicitly include requirement traceability, we are able to provide a practical, scalable and reliable approach.
|
2 |
Contributions à la conception à base de modèles des systèmes temps réel en vue de leur analyse de performance temporelle / Contributions to Model-Based Design of Real-Time Systems Regarding their Timing Performance AnalysisBui Long, Anh Toan 20 December 2018 (has links)
La validation temporelle des systèmes temps réel est nécessaire dans le cadre d’applications critiques tels l’aéronautique, le spatial ou l’automobile. Il s’agit, dans ces systèmes, de garantir les temps de réponse des tâches ainsi que le déterminisme de leurs communications. En raison de la complexité des systèmes actuels ainsi que de leur criticité, il est nécessaire de mettre en place une démarche de conception réduisant le temps de développement et ainsi le temps de mise en marché (time-to-market), tout en réduisant les risques d’erreurs de conception.Ce contexte rend l’ingénierie dirigée par les modèles particulièrement adaptée au développement de ce type de système. Les contributions de cette thèse partent des constats suivants. Premièrement, malgré la multitude des modèles d’analyses existants les modèles actuels ne peuvent retranscrire de nombreux cas rencontrés en industrie. Pour pouvoir analyser ces cas, il est nécessaire de les adapter `a l’analyse. Le deuxième constat porte sur l’adaptation qui n’est toujours pas simple surtout quand il existe une disparité sémantique entre les langages de description d’architecture et les modèles d’analyse ce qui nécessite de les rapprocher. Le dernier constat porte sur les difficultés dans la modélisation des systèmes distribués complexes car à moins de connaître le système complet, la représentation globale et sa validation temporelle reste coûteuse.Cette thèse propose des outils et méthodes pour améliorer le processus de modélisation et d’analyses temps réel. La première contribution consiste en la mise en place d’un référentiel de transformation de modèles endogène pour effectuer une adaptation conservative des modèles industriels aux modèles d’analyses. Dans l’optique de réduire l’écart sémantique entre les langages de description et les modèles d’analyse, cette thèse propose également une modélisation incrémentale des réseaux temps réel en vue de leur validation temporelle car les langages existants les considèrent de fa¸con limitée. La troisième contribution de la thèse porte sur la réduction des artéfacts de modélisation par extraction et élagage de méta-modèles afin d’obtenir les éléments nécessaires par rapport au points de vue d’analyse souhait´es.Toutes ces contributions sont implémentées dans des frameworks intégrant les processus d’analyses temps réel tels Time4Sys et MoSaRT et utilisées, dans le cadre d’un projet collaboratif, par des partenaires industriels. / The timing validation of real-time systems is mandatory for critical applications such as aeronautics,aerospace or automotive systems. The aim is to guarantee tasks response time and messages transmission time on networks. As for the criticality of these complex systems, it is necessary to implement a design process that reduces the development time therefore the time-to-market while reducing design errors risks.This context makes model-driven engineering well adapted for the development of critical real-time systems.The contributions of this thesis rely on the following observations. First of all, despite the existence of various analysis models, they often cannot represent perfectly some industrial cases. To analyze these cases,an adaptation is required to make them analyzable with existing tests. However, the adaptation is not quite easy especially in case of a semantic gap between systems description languages and analysis models. Also,several difficulties have been noticed to design and analyze an entire distributed complex system in one-shot unless knowing well the full system.In this PhD thesis, tools and methods are proposed to ease and improve the modeling and analysis processes of real-time systems. The first thesis contribution consists of implementing a rule-based endogenous transformation repository dedicated to adapt conservatively industrial models to the analysis models. The second contribution is focused on real-time networks and is dedicated to reduce the semantic gap between description languages and analysis models by proposing artefacts allowing to design networks on an incremental way. Moreover, this thesis proposes to reduce modeling artifacts using extraction and meta-models pruning inorder to retrieve useful elements referring to chosen analysis viewpoints.All these contributions are implemented in modeling frameworks integrating real-time analyses processes such as Time4Sys and MoSaRT, and used in a collaborative project by industrial partners.
|
3 |
Analysing and supporting the reliability decision-making process in computing systems with a reliability evaluation framework / Analyser et supporter le processus de prise de décision dans la fiabilité des systèmes informatiques avec un framework d'évaluation de fiabilitéKooli, Maha 01 December 2016 (has links)
La fiabilité est devenu un aspect important de conception des systèmes informatiques suite à la miniaturisation agressive de la technologie et le fonctionnement non interrompue qui introduisent un grand nombre de sources de défaillance des composantes matérielles. Le système matériel peut être affecté par des fautes causées par des défauts de fabrication ou de perturbations environnementales telles que les interférences électromagnétiques, les radiations externes ou les neutrons de haute énergie des rayons cosmiques et des particules alpha. Pour les systèmes embarqués et systèmes utilisés dans les domaines critiques pour la sécurité tels que l'avionique, l'aérospatiale et le transport, la présence de ces fautes peut endommager leurs composants et conduire à des défaillances catastrophiques. L'étude de nouvelles méthodes pour évaluer la fiabilité du système permet d'aider les concepteurs à comprendre les effets des fautes sur le système, et donc de développer des produits fiables et sûrs. En fonction de la phase de conception du système, le développement de méthodes d'évaluation de la fiabilité peut réduire les coûts et les efforts de conception, et aura un impact positif le temps de mise en marché du produit.L'objectif principal de cette thèse est de développer de nouvelles techniques pour évaluer la fiabilité globale du système informatique complexe. L'évaluation vise les fautes conduisant à des erreurs logicielles. Ces fautes peuvent se propager à travers les différentes structures qui composent le système complet. Elles peuvent être masquées lors de cette propagation soit au niveau technologique ou architectural. Quand la faute atteint la partie logicielle du système, elle peut endommager les données, les instructions ou le contrôle de flux. Ces erreurs peuvent avoir un impact sur l'exécution correcte du logiciel en produisant des résultats erronés ou empêcher l'exécution de l'application.Dans cette thèse, la fiabilité des différents composants logiciels est analysée à différents niveaux du système (en fonction de la phase de conception), mettant l'accent sur le rôle que l'interaction entre le matériel et le logiciel joue dans le système global. Ensuite, la fiabilité du système est évaluée grâce à des méthodologies d'évaluation flexible, rapide et précise. Enfin, le processus de prise de décision pour la fiabilité des systèmes informatiques est pris en charge avec les méthodes et les outils développés. / Reliability has become an important design aspect for computing systems due to the aggressive technology miniaturization and the uninterrupted performance that introduce a large set of failure sources for hardware components. The hardware system can be affected by faults caused by physical manufacturing defects or environmental perturbations such as electromagnetic interference, external radiations, or high-energy neutrons from cosmic rays and alpha particles.For embedded systems and systems used in safety critical fields such as avionic, aerospace and transportation, the presence of these faults can damage their components and leads to catastrophic failures. Investigating new methods to evaluate the system reliability helps designers to understand the effects of faults on the system, and thus to develop reliable and dependable products. Depending on the design phase of the system, the development of reliability evaluation methods can save the design costs and efforts, and will positively impact product time-to-market.The main objective of this thesis is to develop new techniques to evaluate the overall reliability of complex computing system running a software. The evaluation targets faults leading to soft errors. These faults can propagate through the different structures composing the full system. They can be masked during this propagation either at the technological or at the architectural level. When a fault reaches the software layer of the system, it can corrupt data, instructions or the control flow. These errors may impact the correct software execution by producing erroneous results or prevent the execution of the application leading to abnormal termination or application hang.In this thesis, the reliability of the different software components is analyzed at different levels of the system (depending on the design phase), emphasizing the role that the interaction between hardware and software plays in the overall system. Then, the reliability of the system is evaluated via a flexible, fast, and accurate evaluation framework. Finally, the reliability decision-making process in computing systems is comprehensively supported with the developed framework (methodology and tools).
|
4 |
Conception sûre des systèmes mécatroniques intelligents pour des applications critiquesBelhadaoui, Hicham 13 January 2011 (has links) (PDF)
La criticité des systèmes complexes programmables nécessite de garantir un niveau de fiabilité et de sécurité convenable. Des études de sûreté de fonctionnement doivent être menées tout au long du cycle de développement du système. Ces études permettent une meilleure maîtrise des risques et de la fiabilité. Les points faibles sont mis en évidence et permettent aux concepteurs de spécifier des stratégies de reconfiguration avant la phase de prototype réel et les tests réels. Les études de sûreté de fonctionnement doivent être menées au plus tôt dans la phase de conception, afin de réduire les coûts et le nombre de prototypes nécessaires à la validation du système. Le travail présenté dans ce mémoire de thèse a pour objectif de définir une méthodologie de conception des systèmes complexes programmables dédiés à une application mécatronique [Belhadaoui et al., 2008-a], intégrant dès les premières phases du cycle de développement [Aït-Kadi et al., 2000], les aspects sûreté de fonctionnement. L'apport d'une telle méthodologie doit permettre de faire face à un certain nombre de contraintes propres au domaine des capteurs intelligents (les exigences de cahier des charges, le respect des normes législatives en vigueur). La méthodologie développée doit permettre de : Modéliser et simuler les comportements fonctionnels et dysfonctionnels des systèmes Estimer la fiabilité par modélisation Réaliser des mesures de sensibilité afin de connaître la contribution de chaque composant à la fiabilité du système Capitaliser la connaissance sur le système au cours des différentes phases d'évaluation (prévisionnelle, expérimentale et opérationnelle) pour affiner les estimations de fiabilité Ce Travail introduit le concept d'information en sûreté de fonctionnement. Nous interprétons la défaillance de celle-ci comme étant le résultat de l'initiation et de la propagation d'informations erronées à travers l'architecture d'un capteur intelligent dédié à une application mécatronique. Cette propagation s'est accompagnée de contraintes (partage de ressources matérielles et informationnelles, modes dégradés d'information...) qui tendent à influencer fortement la crédibilité de cette information. Nous débutons sur un état de l'art pour montrer l'intérêt de l'approche flux informationnel sur un cas d'étude complexe. Ceci est lié à la présence d'une partie programmable (interaction matériel-logiciel) et évidement du système hybride (signaux mixtes analogique-numérique). Cette nouvelle approche distingue, les phénomènes d'apparition et de disparition d'erreurs (matérielles, logicielles et environnementales), ainsi que les séquences de propagation aboutissant à un mode de dysfonctionnement du système. Grâce à cette distinction nous expliquons les concepts mal traités par les méthodes conventionnelles, tels que la défaillance simultanée, la défaillance de cause commune et abordons d'une manière réaliste les problématiques des interactions matériel-logiciel et celle des signaux mixtes. Les séquences de propagation d'erreurs générées permettent à l'aide d'un modèle markovien non homogène, de quantifier d'une manière analytique les paramètres de la sûreté de fonctionnement du système (fiabilité, disponibilité, sécurité) et de positionner le capteur dans un mode de fonctionnement parmi les six que nous avons définis suivant les spécifications du cahier des charges.
|
5 |
Sécurités (immunité et innocuité) des architectures ouvertes à niveaux de criticité multiples : application en avioniqueLaarouchi, Youssef 30 November 2009 (has links) (PDF)
La conception et le développement des applications critiques en avionique sont soumis à des contraintes strictes visant à assurer un niveau de confiance compatible avec les exigences de sécurité-innocuité (au sens safety) des tâches mises en Suvre. Ces contraintes induisent un accroissement considérable des coûts de production et de maintenance, ce qui rend le prix de revient de tels systèmes prohibitif. D'un autre côté, les composants sur étagère (Commercial Off-The-Shelf, COTS), matériels et logiciels, sont maintenant d'usage courant et offrent des services étendus pour un coût faible. Cependant, les COTS ne répondent pas aux contraintes d'innocuité exigées pour les tâches critiques ; de plus, ils présentent des vulnérabilités facilement exploitables par des attaques, les rendant incompatibles avec des exigences élevées de sécurité-immunité (au sens security). Il serait toutefois intéressant de profiter de tels composants dans un contexte avionique, mais en faisant en sorte qu'ils ne puissent affecter de façon préjudiciable les tâches critiques. Intégrer de tels composants dans les systèmes avioniques conduit donc à prendre en considération l'hétérogénéité des niveaux de confiance entre d'une part les applications critiques classiques, et d'autre part de nouvelles applications utilisant des composants sur étagère. Dans le cadre de cette thèse, nous proposons une architecture autorisant de telles interactions tout en préservant les propriétés de safety et security. La définition de cette architecture s'appuie sur le modèle Totel, et elle utilise la virtualisation afin de faciliter la mise en Suvre des mécanismes de tolérance aux fautes destinés à augmenter la crédibilité d'une application exécutée de façon répliquée sur des plateformes d'exécution COTS de niveau de confiance faible. Afin de valider notre approche, nous avons réalisé un prototype en nous appuyant sur deux cas d'étude identifiés avec Airbus et concernant tous deux des ordinateurs portables : un dédié à la maintenance et un au calcul du profil de décollage d'un avion.
|
6 |
Algorithmes et architectures pour la commande et le diagnostic de systèmes critiques de vol / Algorithms and architectures for control and diagnosis of flight critical systemsBobrinskoy, Alexandre 29 January 2015 (has links)
Les systèmes critiques de vol tels que les actionneurs électromécaniques ainsi que les calculateurs de commande moteur (ECU) et de vol (FCU),sont conçus en tenant compte des contraintes aéronautiques sévères de sureté defonctionnement. Dans le cadre de cette étude, une architecture calculateur pourla commande et la surveillance d’actionneurs moteur et de surfaces de vol est proposée et à fait l’objet d’un brevet [13]. Pour garantir ces mesure de sureté, les ECU et FCU présentent des redondances matérielles multiples, mais engendrent une augmentation de l’encombrement, du poids et de l’énergie consommée. Pour ces raisons, les redondances à base de modèles dynamiques, présentent un atout majeur pour les calculateurs car elles permettent dans certains cas de maintenir les exigences d’intégrité et de disponibilité tout en réduisant le nombre de capteurs ou d’actionneurs. Un rappel sur les méthodes de diagnostic par générateurs de résidus et estimateurs d’états [58, 26, 47] est effectué dans cette étude. Les propriétés de platitude différentielle et la linéarisation par difféomorphisme et bouclage endogène [80, 41, 73] permettent d’utiliser des modèles linéaires équivalents avec les générateurs de résidus. Un banc d’essai a été conçu afin de valider les performances des algorithmes de diagnostic. / Flight-Critical Systems such as Electromechanical Actuators driven by Engine Control Units (ECU) or Flight Control Units (FCU) are designed and developed regarding drastic safety requirements. In this study, an actuator control and monitoring ECU architecture based on analytic redundancy is proposed. In case of fault occurrences, material redundancies in avionic equipment allow certaincritical systems to reconfigure or to switch into a safe mode. However, material redundancies increase aircraft equipment size, weight and power (SWaP). Monitoring based on dynamical models is an interesting way to further enhance safetyand availability without increasing the number of redundant items. Model-base dfault detection and isolation (FDI) methods [58, 26, 47] such as observers and parity space are recalled in this study. The properties of differential flatness for nonlinear systems [80, 41, 73] and endogenous feedback linearisation are used with nonlinear diagnosis models. Linear and nonlinear observers are then compared with an application on hybrid stepper motor (HSM). A testing bench was specially designed to observe in real-time the behaviour of the diagnosis models when faults occur on the stator windings of a HSM.
|
7 |
Détection d'erreur au plus tôt dans les systèmes temps-réel : une approche basée sur la vérification en ligne / Early error detection for real time applications : an approach using runtime verificationRobert, Thomas 26 June 2009 (has links)
La vérification en ligne de spécifications formelles permet de créer des détecteurs d'erreur dont le pouvoir de détection dépend en grande partie du formalisme vérifié à l'exécution. Plus le formalisme est puissant plus la séparation entre les exécutions correctes et erronées peut être précise. Cependant, l'utilisation des vérifieurs en-ligne dans le but de détecter des erreurs est entravée par deux problèmes récurrents : le coût à l'exécution de ces vérifications, et le flou entourant les propriétés sémantiques exactes des signaux d'erreur ainsi générés. L'objectif de cette thèse est de clarifier les conditions d'utilisation de tels détecteurs dans le cadre d'applications « temps réel » critiques. Dans ce but, nous avons donné l'interprétation formelle de la notion d'erreur comportementale « temps réel». Nous définissions la propriété de détection « au plus tôt » qui permet de d'identifier la classe des détecteurs qui optimisent la latence de détection. Pour illustrer cette classe de détecteurs, nous proposons un prototype qui vérifie un comportement décrit par un automate temporisé. La propriété de détection au plus tôt est atteinte en raisonnant sur l'abstraction temporelle de l'automate et non sur l'automate lui-même. Nos contributions se déclinent dans trois domaines, la formalisation de la détection au plus tôt, sa traduction pour la synthèse de détecteurs d'erreur à partir d'automate temporisés, puis le déploiement concret de ces détecteurs sur une plate-forme de développement temps réel, Xenomai. / Runtime verification of formal specifications provides the means to generate error detectors with detection capabilities depending mostly on the kind of formalism considered. The stronger the formalism is the easier the speration between correct and erroneous execution is. Nevertheless, two recurring issues have to be considered before using such error detection mechanisms. First, the cost, at run-time, of such error detector has to be assessed. Then, we have to ensure that the execution of such detectors has a well defined semantics. This thesis aims at better understanding the conditions of use of such detectors within critical real-time software application. Given formal behavioural specification, we defined the notion of "behavioural error". Then, we identify the class of early detectors that optimize the detection latency between the occurence of such errors and their signalling. The whole generation process has been implemented for specifications provided as timed automata. The prototype achieves early error detection thanks to a preprocessing of the automaton to generate its temporal abstraction. Our contributions are threefold : formalisation of early detection, algorithms for timed automata run-time verification, and prototyping of such detectors on a real-time kernel, Xenomai.
|
8 |
Génération de tests à partir de modèle UML/OCL pour les systèmes critiques évolutifsFourneret, Elizabeta 05 December 2012 (has links) (PDF)
Cette thèse porte sur l'étude d'une démarche et de techniques pour prendre en compte les spécificités des systèmes sécurisés évolutifs lors de la génération des tests à partir de modèles UML/OCL. Dans ce travail, trois axes sont étudiés : (i) le cycle de vie des tests, (ii) les exigences fonctionnelles et (iii) les exigences de sécurité. Dans un premier temps, nous avons défini la clé de voûte de notre approche qui est la caractérisation des statuts du cycle de vie des tests. À l'issu de ces travaux, nous avons pu définir la démarche de classification des tests pour les systèmes évolutifs, appelée SeTGaM. La notation UML, accompagnée du langage de spécification OCL, permet de formaliser les comportements du système. Le langage OCL spécifie ainsi les gardes/actions des transitions et les pré/post conditions des opérations. La méthode propose ainsi deux classifications des tests : la première s'appuie sur les comportements issus des transitions du diagramme d'états/transitions, tandis que l'autre repose sur l'étude des comportements issus des opérations du diagramme de classes. Dans le domaine du test de logiciels critiques, une des questions clés concerne la sécurité. Pour cette raison, nous avons enrichi l'approche SeTGaM en prenant en compte l'aspect sécurité. Ainsi, SeTGaM permet de générer sélectivement des tests qui ciblent les différentes exigences de sécurité lors des évolutions du système. Finalement, le prototype de SeTGaM a été intégré, avec l'outil Smartesting CertifyIt, à l'environnement IBM Rational Software Architect. Ceci nous a permis de valider expérimentalement le passage à l'échelle de la méthode sur des études de cas industriels, notamment proposées par Gemalto/Trusted Labs dans le cadre du projet européen SecureChange.
|
9 |
Architecture sécurisée pour les systèmes d'information des avions du futurLastera, Maxime 04 December 2012 (has links) (PDF)
Traditionnellement, dans le domaine avionique les logiciels utilisés à bord de l'avion sont totalement séparés des logiciels utilisés au dehors afin d'éviter toutes interaction qui pourrait corrompre les systèmes critiques à bord de l'avion. Cependant, les nouvelles générations d'avions exigent plus d'interactions avec le monde ouvert avec pour objectif de proposer des services étendu, générant ainsi un flux d'information potentiellement dan- gereux. Dans une précédente étude, nous avons proposé l'utilisation de la virtualisation pour assurer la sûreté de fonctionnement d'applications critiques assurant des communi- cations bidirectionnelles entre systèmes critiques et systèmes non sûr. Dans cette thèse nous proposons deux contributions. La première contribution propose une méthode de comparaison d'hyperviseur. Nous avons développé un banc de test permettant de mesurer les performances d'un système virtualisé. Dans cette étude, différentes configurations ont été expérimentées, d'un système sans OS à une architecture complète avec un hyperviseur et un OS s'exécutant dans une machine virtuelle. Plusieurs tests (processeur, mémoire et réseaux) ont été mesurés et collectés sur différents hyperviseurs. La seconde contribution met l'accent sur l'amélioration d'une architecture de sécurité existante. Un mécanisme de comparaison basé sur l'analyse des traces d'exécution est utilisé pour détecter les anomalies entre instances d'application exécutées sur diverse ma- chines virtuelles. Nous proposons de renforcer le mécanisme de comparaison à l'exécution par l'utilisation d'un modèle d'exécution issu d'une analyse statique du bytecode Java. Afin de valider notre approche, nous avons développé un prototype basé sur un cas d'étude identifié avec Airbus qui porte sur l'utilisation d'un ordinateur portable dédié à la maintenance.
|
10 |
Automatisation de la Certification Formelle de Systèmes Critiques par Instrumentation d'Interpréteurs AbstraitsGarnacho, Manuel 27 August 2010 (has links) (PDF)
Mes travaux de doctorat ont porté sur la certification de programmes impératifs utilisés dans des applications critiques. Les certificats établissent la validité des propriétés sémantiques des programmes et sont produits sous forme de preuves déductives vérifiables par machine. Le défi relevé dans cette thèse est d'automatiser la construction des preuves de correction de programmes. Nous avons suivie l'approche de Floyd-Hoare pour prouver que les propriétés sémantiques sont des invariants du programme et nous avons utilisé le le système Coq pour vérifier la validité des preuves. On considére ici le cas où les propriétés sémantiques sont calculées par des analyseurs statiques de programmes qui s'appuient sur la théorie de l'interprétation abstraite. Nous proposons une méthode d'instrumentation des analyseurs statiques de programmes afin de leur faire générer automatiquement un certificat pour chaque propriété sémantique calculée. L'instrumentation consiste à associer à certaines fonctions d'un analyseur statique des patrons de preuve qui à l'exécution généreront les certificats. De tels analyseurs instrumentés ne sont pas pour autant certifiés puisque leur correction pour toutes leurs entrées possibles n'est pas garantie, néanmoins ils sont capables de justifier par une preuve formelle la correction du résultat de chacun de leurs calculs. Bien sûr, si pour une entrée possible l'exécution de l'analyseur est boguée le résultat sera erroné et la justification produite ne sera pas une preuve valide; elle sera rejettée par le vérificateur de preuves. Cette approche permet de certifier avec un très haut-niveau de confiance (celui du vérificateur de preuves) les résultats d'outils existants, même à l'état de prototypes. Pour que l'instrumentation soit applicable en pratique, nous avons cherché à limiter le nombre de fonctions à instrumenter. Nous avons dégagé un ensemble restreint de fonctions, commun à tout analyseur, à instrumenter pour qu'un analyseur existant devienne un outil de certification automatique. Nous avons appliqué cette technique d'instrumentation à un analyseur de programmes manipulant des tableaux qui s'appuie sur des domaines abstraits non triviaux. Cet analyseur calcule des propriétés sur le contenu des tableaux manipulés par les programmes et, grâce à notre instrumentation, génère désormais des certificats vérifiables par Coq attestant de la validité des propriétés découvertes par l'analyse statique. Nous montrons enfin comment utiliser cet analyseur instrumenté pour certifier un protocole de communication pour systèmes multi-tâches destiné à l'avionique. La garantie de la correction des programmes est cruciale dans le domaine des systèmes embarqués. Face aux coûts et la durée d'une procédure de certification formelle, le développement d'outils automatiques de certification représente un enjeu économique majeur. La transformation, par instrumentation, d'outils d'analyses existants en outils de certification est une réponse possible qui évite la certification des outils d'analyse.
|
Page generated in 0.0734 seconds