of 37

Études et développement de diagrammes de décision linéaires

0 views
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Share
Description
Études et développement de diagrammes de décision linéaires Annie Ressouche, Daniel Gaffé, Dorine Havayarimana To cite this version: Annie Ressouche, Daniel Gaffé, Dorine Havayarimana. Études et développement
Transcript
Études et développement de diagrammes de décision linéaires Annie Ressouche, Daniel Gaffé, Dorine Havayarimana To cite this version: Annie Ressouche, Daniel Gaffé, Dorine Havayarimana. Études et développement de diagrammes de décision linéaires. Informatique et langage [cs.cl] hal HAL Id: hal Submitted on 16 Dec 2017 HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers. L archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d enseignement et de recherche français ou étrangers, des laboratoires publics ou privés. Université de Nice Sophia Antipolis Institut National de Recherche en Informatique et Automatique Rapport de stage Études et développement de diagrammes de décisions linéaires Stagiaire Havyarimana Dorine Filiaire Master II Électronique, Systèmes et Télécommunications Sous la direction de : Annie Ressouche Daniel Gaffé 10 Avril Septembre 2017 Pour Carmen et Paulin... Empower yourself with a good education, then get out there and use that education to build a country worthy of your boundless promise. Michelle Obama 1 Résumé La vérification de modèle, plus communément appelé Model Checking, est un concept basé sur une approche automatique de vérification formelles des propriétés temporelles sur des systèmes réactifs. INRIA en collaboration avec le LEAT ont développé CLEM, un outil de modélisation et de vérification de propriétés, s appuyant sur une représentation d état en automates finis générés automatiquement et représentés par des Diagrammes de Décisions Binaires. Dans une optique d évolution, le travail effectué durant ce stage a été de développer la bibliothèque de diagramme de décision linéaire, nous nous sommes concentrés sur l inclusion de nouvelles méthodes de réduction dans les cas d implication forte et faible. L objectif de ce travail est de développer la partie vérification de CLEM en remplaçant la représentation actuelle des valeurs fondamentales qui utilisent des diagrammes de décisions binaires(bdds) par les diagrammes de décisions linéaires(ldds) ce qui nous permettrait de représenter les états par des valeurs entières et non par des signaux non comparables entre eux. Cette nouvelle bibliothèque de LDDs, une fois implémentée sur CLEM, permettra de faire des vérifications de modèles plus fines et, potentiellement, le rendra plus performant. 2 Abstract Model verification, more commonly known as Model Checking, is a concept based on an automatic formal verification approach of temporal properties on reactive systems. INRIA in collaboration with LEAT developed CLEM, a modeling and property verification tool, based on a state representation in finite automata generated automatically using binary decisions diagrams. From an evolutionary point of view, the work carried out during this internship was to develop the library of linear decisions diagrams, we focused on the implementation of new reduction methods in cases of Imply High and Imply Low case. The objective of this work is to develop the verification part of CLEM by replacing the representation of the fundamental values using binary decisions diagrams(bdds) with linear decisions diagrams(ldds) which will allow us to represent the states by integer values instead of signals which are not comparable among themselves. This new library, once implemented on CLEM, will make checks of finer models and, we hope, will make it more powerful. 3 Remerciements Je voudrais remercier mes encadrants Annie Ressouche et Daniel Gaffé qui m ont permis de faire ce stage, je n oublierai jamais ces 6 mois de travail, de surpassement de soi. Vous m avez offert la connaissance, c est un trésor que je chérirai et entretiendrai tout au long de ma vie. A tout les membres de l équipe STARS, en particulier les stagiaires, nous avons bien travaillé ensemble mais nous avons également profité de moments d échanges et de complicité autour de dîners et pique-niques magnifiques. Mon moment préféré : les feux d artifice à Cannes! (Joyeux anniversaire Inès!) A ma famille de cœur de France, d Algérie, du Rwanda, du Burundi. A Séverine et sa maman pour leur soutien moral, une vie ne suffirait pas pour leur rendre la pareille. A Carmelle, Dorelle, Lolita, Lynda, Marlyne, Véra mes amies de toujours. A Khélia, qui a toujours été là pour moi durant nos années en Algérie, j espère qu on se reverra bientôt et que la médecine te rend heureuse. Cette page ne suffirait pas pour exprimer ma gratitude envers cette personne qui a rendu mon monde si loin de tout les êtres qui me sont chères aussi incroyable et peuplé de magnifiques aventures. Merci à toi Lyes Khacef, le Kabyle partisan de la liberté, de l expression de soi ; bref, de la vérité. Tu accompliras des choses extraordinaires. A Mathys et ses parents Claire et Didi, Franco mon cousin pour leur courage qui me rappelle à chaque fois que rien n est impossible. Merci pour votre soutien. A mes parents Césarie et Pierre, mon frère Elvis et mes sœurs Carmen et Marlyn, je vous aime. 4 Table des matières Résumé Abstract Remerciements Introduction générale Vue d ensemble du sujet de recherche Présentation de l organisme d accueil : INRIA INRIA Sophia Antipolis Présentation de l équipe projet STARS Le projet NeuComp État de l art Les bugs Le Model Checking L interprétation abstraite Les types de représentation abstraite Les polyèdres Les diagrammes de décisions linéaires Introduction Structure des LDDs Les règles de réduction des LDDs Réduction par implication forte ou faible Inclusion de nouvelles combinaisons dans les LDDs Conclusion générale 32 A Démonstration 34! = 0 sur 32 bits 33 5 Table des figures 1.1 Système réactif Exemple de fausse causalité dans CLEM en (1) et version acceptée par CLEM. a est le signal représentant x 9 et b le signal représentant x 9 [Abd14] Schéma de compilation de CLEM Exemple d un bug du programme factoriel, vous trouverez en annexe une démonstration de l origine de ce bug Approche d un model checker Représentation abstraite selon Cousot [Cou78] Type de représentation abstraite extrait de la thèse de Antoine Miné [Min04] Représentation d un LDD sous forme de polyèdre Représentation de F1 sous forme de LDD + avec n = Représentation de F2 sous forme de LDDs + avec n = Représentation de F1 et F2 dans le domaine abstrait(le nombre d arêtes correspond à la valeur de n) Réduction des LDDs : Cas des implications fortes (1) et faibles (3) Inclusions des combinaisons Représentation du LDD à l aide des zones Premier cas Deuxième cas Troisième cas Quatrième cas Représentation générale des 4 cas Liste des tableaux 3.1 Liste des contraintes LDDs de F Liste des contraintes LDDs de F Recombinaison des contraintes LDDs de F Recombinaison des contraintes LDDs de F List of Algorithms 1 implyhigh(lddnode u) implylow(lddnode u) Réduction en cas de recombinaison par addition et/ou soustraction (exemple du cas 3.8) Chapitre 1 Introduction générale L informatique des capteurs dite aussi informatique omniprésente trouve son origine dans une génération naissante d appareils électroniques publics équipés de capteurs qui est, et sera encore plus, en mesure d observer, analyser et interpréter les informations reçues par ces capteurs. Les systèmes réactifs, autrement dit les systèmes dont l état et le comportement change en fonction de l évolution temporelle des entrées, sont des systèmes qui se trouvent représenter aussi bien en Science de la Vie qu en Science de l Ingénieur, de la Matière et même en Sciences Humaines ; d intenses recherches expérimentales et théoriques ont vu le jour afin de comprendre et prédire leur évolution. Figure 1.1: Système réactif La caractéristique principale de ces systèmes est d être capable de définir un nombre de comportements infini grâce aux multiples interactions des éléments qui le composent ; ce qui rend leur conception et mise en œuvre extrêmement difficile. De tels systèmes ont un rôle assez souvent critique (centrales nucléaire, poste de contrôle avionique) qui oblige les concepteurs à passer par une phase coûteuse mais indispensable de test pour éviter d éventuels dysfonctionnements du système et des exemples sont donnés ici pour témoigner de l importance de la phase de vérification : 9 1. Le Missile de défense Patriot rencontre un problème de logiciel qui conduit à l échec du système [Arn91] Un calcul inexact du temps en raison d erreurs arithmétiques informatiques a causé la mort de 28 soldats et blessé 100 autres en Arabie Saoudite. 2. Destruction du vol 5.01 d Ariane en 1996 [La96] L incident a été provoqué par une erreur dans le logiciel de contrôle qui a effectué une conversion de données à partir d un système flottant de 64 bits en un entier signé de 16 bits, faisant croire à l ordinateur de bord qu il fallait inverser la poussée! Cet incident a coûté 500 Millions de dollars Rappel de centaines de milliers de Pentium Intel en 1994 Une erreur de conception dans la gestion de la retenue de la division flottante a conduit Intel à inventer le premier processeur qui calcule faux... Pour des systèmes réactifs dits critiques, l erreur est interdite (contrôle d une centrale nucléaire, télé-paiement par carte à puce, etc.). Approcher la réalité des phénomènes temporels de ces systèmes est un vrai challenge scientifique qui, associé au progrès technologiques réalisés au cours de ces dernières décennies ainsi que l apparition de capteurs dit «intelligents», engendre un besoin de développer des outils de vérification formelles permettant une représentation des systèmes complexes pouvant répondre aux impératifs de sécurité. Les systèmes critiques qu ils soient hardware ou software peuvent bénéficier d une phase de validation sous différentes méthodes : La simulation Les tests La vérification formelle basée sur les méthodes déductives La vérification formelle basée sur le Model Checking La vérification formelle basée sur l interprétation abstraite Les méthodes de tests et de simulation sont les plus classiquement utilisées mais elles présentent un inconvénient majeur, car il est souvent impossible de tester tous les états possibles d un système : l ensemble des cas à tester doit être minutieusement choisi afin de couvrir le maximum de scénarios possibles. La méthode de vérification formelle repose sur une représentation des états possibles du système par le biais d outils mathématiques. Elle propose une approche rigoureuse de la programmation où l on a : Une représentation mathématique du système. Une propriété du système à vérifier. Un algorithme de vérification du système. Tout ceci dans l objectif de prouver les propriétés fondamentales de : Sûreté c est à dire que jamais rien de nuisible au système ou à l environnement humain n arrive! Vivacité c est à dire que le programme effectue les taches qui lui sont confiées de manière prédictible. En d autres termes, indépendemment des états précédents du système, si celui-ci arrive dans un état donné et reçoit une entrée donnée, son évolution sera toujours prédictible. La production de systèmes logiciels fiables constitue l une des préoccupations majeures des informaticiens qui, pour faire face à la grande évolution technologique de ce siècle, doivent développer des méthodes et outils de vérification de systèmes encore plus performants. La 10 vérification formelle par Model Checking est l une des méthodes les plus utilisées car elle permet une vérification simple, efficace, exhaustive mais surtout complètement automatisable. Ce qui la rend avantageuse par rapport aux autres méthodes. Afin d être intégré à l outil de vérification de CLEM, un modèle mathématique des programmes s appuyant sur une bibliothèque de diagrammes de décisions binaires est en développement sous la forme de diagrammes de décisions linéaires. L objectif de ce travail est de contribuer à l amélioration de la bibliothèque de diagrammes de décisions linéaires, qui sera par la suite intégrée dans le compilateur CLEM. 1.1 Vue d ensemble du sujet de recherche Ce stage a été effectué au sein de l INRIA dans le cadre du projet Bio-informatique Neu- Comp, qui a pour objectif de modéliser et vérifier les propriétés temporelles du modèle Leaky Integrate and Fire [LIF], un modèle de neurone à Spike. Un travail de recherche [DMMG + 16] avait été effectué par mes encadrants afin de modéliser et vérifier un réseau de neurones en utilisant le langage synchrone Lustre. Ce travail a permit de représenter des architectures neuronales ainsi que la vérification de quelques propriétés par Model Checking. CLEM [GR13], un compilateur en langage synchrone Light Esterel[RGR08] développé à l origine dans l objectif de synthétiser des automates explicites en une machine implicite de Mealy ou Moore, est utilisé pour interpréter les systèmes réactifs en un modèle bien structuré et facilite l analyse et le test dans la suite afin de simplifier le travail des Model Checkers qui prouvent des propriétés de logique temporelle sur un modèle du programme représenté sous forme d équations booléennes et de registres. Le problème de ce type de vérification est qu il ne marche que si nous sommes dans le monde booléen. Lorsque nous voulons représenter des contraintes sur des valeurs, nous sommes obligés de donner une représentation abstraite du système (donc incomplète) sous forme booléenne. Par exemple, si tout un ensemble de code est conditionné par la condition x 9 and x = 9 tel que x soit une variable entière, CLEM va introduire deux signaux booléens data1 et data2 représentant respectivement chaque contrainte élémentaire. Il conditionnera ensuite le groupe de codes associé par data1 and data2 . Or data1 et data2 sont opposés, donc l expression data1 and data2 vaut toujours 0 : Tout le groupe de codes associé forme donc du code mort qui va quand même être généré par le compilateur CLEM... Ce code va également compliquer a posteriori la vérification de propriétés globales du système alors qu il n a aucune influence... (Voir 1.2) C est un des exemples de comportement dans CLEM qui pourrait trouver une interprétation différente grâce à l implémentation de diagrammes de décisions linéaires. La vision de ce stage est de contribuer à la conception d un nouveau model checker inspiré de ceux utilisés par CLEM, qui s appuierait sur une représentation sous forme de diagrammes de décisions linéaires. Cette représentation permettra d identifier des intervalles de valeurs entières dans lesquelles une propriété est vérifiée. Les diagrammes de décision linéaires étant des représentations permettant une interprétation abstraite du système, l étude bibliographique est orientée dans ce sens. Nous nous sommes également appuyés sur une bibliothèque représentant un autre type de diagrammes de décisions linéaires développée en 2009 par Chaki, Gurfinkel et Strichman [CGS09] afin de faire apparaître certains principes de réduction dans les nouveaux diagrammes de décision linéaires qui sont identiques aux anciens. 11 Nous appellerons dans ce rapport LDD(s) les diagrammes de décisions linéaires selon [CGS09] et LDD + (s) les diagrammes de décision linéaires sur lesquels nous avons travaillés. Figure 1.2: Exemple de fausse causalité dans CLEM en (1) et version acceptée par CLEM. a est le signal représentant x 9 et b le signal représentant x 9 [Abd14] Figure 1.3: Schéma de compilation de CLEM 12 1.2 Présentation de l organisme d accueil : INRIA L Institut National de Recherche en Informatique et Automatique(INRIA) [INR], qui fete cette année ses 50 ans, est un établissement public français à caractère scientifique et technologique (EPST), qui a été créé à Rocquencourt en 1967, et qui s est étendu sur huit sièges répartis sur tout le territoire français (Rocquencourt, Bordeaux, Grenoble, Lille, Nancy, Rennes, Saclay, et Sophia Antipolis). INRIA est reconnu à l échelle internationale, son but est de produire une recherche d excellence en Mathématiques des Sciences du Numérique, et en Informatique et d assurer son impact. Il a également pour vocation de faire du transfert technologique vers l industrie en supportant financièrement le lancement de StartUps. Aujourd hui, plus de 4000 personnes de différentes nationalités travaillent à l INRIA, dont 3450 scientifiques (1678 chercheurs de l institut et 1778 universitaires ou chercheurs d autres organismes) qui sont regroupés en 172 équipes de recherche réparties dans les huit centres de recherche. Les thèmes de recherche de ces équipes s articulent autour de cinq domaines principaux qui sont : Mathématiques appliquées, calcul et simulation Algorithmique, programmation, logiciels et architectures Réseaux, systèmes et services, calcul distribué Perception, Cognition, Interaction Santé, biologie et planète numérique INRIA Sophia Antipolis INRIA Sophia Antipolis est le troisième site créé par INRIA (après Rocquencourt et Rennes). Il est présent sur la technopole de Sophia Antipolis depuis Plus de 600 personnes travaillent dans ce centre de recherche, et au sein de 32 équipes (dont STARS). Ces équipes poursuivent un bon nombre d engagement avec plusieurs acteurs académiques et économiques (des établissements de recherche, des associations, des entreprises...), et s impliquent dans des réseaux de recherche différents, en s appuyant sur la qualité de ses chercheurs et ses services, afin d ajouter de nouvelles idées innovantes qui enrichissent les domaines de recherche technologiques diversifiés tels que les mathématiques appliquées, les langages de programmation, l algorithmique, les réseaux et systèmes distribués, etc Présentation de l équipe projet STARS L équipe de recherche STARS (Spatio-Temporal Activity Recognition Systems) se concentre sur deux domaines d application : la vidéo-surveillance et le maintien des personnes âgées à domicile. Elle se focalise sur la conception et le développement des systèmes cognitifs pour la reconnaissance d activités. Cette équipe étudie les activités spatio-temporelles à long terme des êtres humains, des véhicules ou des animaux. Cette étude se fait à l aide de l interprétation sémantique et en temps réel de plusieurs scènes dynamiques surveillées par des capteurs et des caméras vidéo. STARS se focalise sur deux axes de recherche principaux qui sont : L interprétation de scènes pour la reconnaissance d activités : Cette interprétation a pour but de trouver une solution pour tout le problème d interprétation, de l analyse bas-niveau du signal jusqu à la description sémantique du contenu de la scène contrôlée par les capteurs et/ou les caméras vidéo. Plus précisément, STARS travaille en perception, interprétation et apprentissage. 13 L architecture logicielle pour la reconnaissance d activités : Ceci consiste à étudier les systèmes génériques pour la reconnaissance d activités, et à élaborer des méthodologies de conception de ces systèmes, en assurant la généricité, la modularité, l extensibilité, la ré-utilisabilité, la fiabilité et la maintenabilité. 1.3 Le projet NeuComp L avancée technologique ouvre des perspectives de recherche énorme dans le domaine des réseaux de neurones artificiels. Afin d orienter ces recherches dans ce domaine en plein essor, l Université Cote d Azur a lancé l académie d excellence «Réseaux, Information et Société Numérique» (RISE). Les objectifs principaux de l académie RISE sont les suivants : L élaboration et l expérimentation de réseaux de communication du futur. L excellence d UCA dans les sciences numériques. Amélioration de la compréhension de la transformation émanant de la numérisation de la société. Depuis le lancement de l académie RISE, 8 projets ont déjà vu le jours : 1. Beyond RRTC 2. DigiCom 3. ElectroSmart 4. Digital Heart (LCN) 5. OPENING 6. UCA4SVR 7. ValueModels 8. NeuComp : C e
Related Search
Advertisements
Related Docs
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks