• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 27
  • 18
  • 3
  • Tagged with
  • 51
  • 51
  • 30
  • 28
  • 26
  • 25
  • 24
  • 24
  • 14
  • 14
  • 12
  • 12
  • 11
  • 9
  • 8
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

Dioïdes et idéaux de polynômes en analyse statique / Static analysis with dioids and polynomial ideals

Jobin, Arnaud 16 January 2012 (has links)
L'analyse statique a pour but de vérifier qu'un programme a le comportement souhaité c.à.d. satisfait des propriétés de sûreté. Toutefois, inférer les propriétés vérifiées par un programme est un problème difficile : le théorème de Rice énonce que toute propriété non triviale d'un langage de programmation Turing-complet est indécidable. Afin de contourner cette difficulté, les analyses statiques effectuent des approximations des comportements possibles du programme. La théorie de l'interprétation abstraite permet de donner un cadre formel à ces approximations. Cette théorie, introduite par Cousot & Cousot propose un cadre d'approximation basé sur la notion de treillis, de connexion de Galois et de calculs de points fixes par itération. Ce cadre permet de définir la qualité des approximations effectuées et notamment la notion de meilleure approximation. À l'opposé, les notions quantitatives n'apparaissent pas naturellement dans ce cadre. Nous nous sommes donc posés la question de l'inférence, par analyse statique, de propriétés s'exprimant de manière quantitative (telles que l'utilisation de la mémoire ou le temps d'exécution). / Static analysis aims to verify that programs behave correctly i.e. satisfy safety properties. However, generating properties verified by a program is a difficult problem : Rice’s theorem states that any non-trivial property about the language recognized by a Turing machine is undecidable. In order to avoid this difficulty, static analyses approximate the possible behaviours of the program. Abtract interpretation theory defines a formal framework for approximating programs. This theory, introduced by Cousot & Cousot is based on the mathematical structure of lattices, Galois connections and iterative fixpoints calculus. This framework defines the notion of correct approximation and allows for qualitatively compare approximations. On the contrary, it is not suitable for handling quantitative properties (such as memory usage and execution time).
2

Analyse statique de programmes manipulant des tableaux

Perrelle, Valentin 21 February 2013 (has links) (PDF)
L'analyse statique de programmes est un domaine crucial en compilation, en optimisation, et en validation de logiciels. Les structures de données complexes (tableaux, listes, graphes,...), omniprésentes dans les programmes, posent des problèmes difficiles, du fait qu'elles représentent des ensembles de données de taille importante ou inconnue, et que l'adressage des données dans ces ensembles est calculé (indexation, indirection). Si la vérification de la validité des accès aux tableaux a été l'une des motivations initiales de l'interprétation abstraite, la recherche de propriétés concernant le contenu des tableaux est quant à lui un sujet récent. La plupart des travaux sur le sujet reposent sur un partitionnement des tableaux. On est ainsi amenés à considérer un certain nombre de fragments de tableau desquels on cherche à trouver des propriétés. Le choix de cette partition est un problème difficile et chacune des méthodes proposées peut être mise en défaut. Par ailleurs, les représentations classiques des partitions de tableau donnent à ces analyses une complexité exponentielle. Nous proposons d'une part de généraliser le concept de partitionnement de tableau à celui de "fragmentation" permettant à la fois le chevauchement des fragments, la manipulation de fragments potentiellement vides et la sélection de relations spécialisées. D'autre part, nous proposons une abstraction de ces fragmentations en terme de graphes appelés "Diagrammes de tranches" ainsi que les opérations pour les manipuler et assurant une complexité polynomiale à l'analyse. Enfin, nous proposons un nouveau critère de fragmentation sémantique inspiré de ceux de la littérature et tentant d'en corriger les défauts. Ces méthodes ont été implémentées dans un analyseur statique. L'expérimentation démontre qu'elles peuvent analyser avec efficacité et précision un certain nombre d'exemples constituant des défis de l'analyse statique de programmes manipulant des tableaux.
3

Dioïdes et idéaux de polynômes en analyse statique

Jobin, Arnaud 16 January 2012 (has links) (PDF)
L'analyse statique a pour but de vérifier qu'un programme a le comportement souhaité c.à.d. satisfait des propriétés de sûreté. Toutefois, inférer les propriétés vérifiées par un programme est un problème difficile : le théorème de Rice énonce que toute propriété non triviale d'un langage de programmation Turing-complet est indécidable. Afin de contourner cette difficulté, les analyses statiques effectuent des approximations des comportements possibles du programme. La théorie de l'interprétation abstraite permet de donner un cadre formel à ces approximations. Cette théorie, introduite par Cousot & Cousot propose un cadre d'approximation basé sur la notion de treillis, de connexion de Galois et de calculs de points fixes par itération. Ce cadre permet de définir la qualité des approximations effectuées et notamment la notion de meilleure approximation. À l'opposé, les notions quantitatives n'apparaissent pas naturellement dans ce cadre. Nous nous sommes donc posés la question de l'inférence, par analyse statique, de propriétés s'exprimant de manière quantitative (telles que l'utilisation de la mémoire ou le temps d'exécution).
4

Certified semantics and analysis of JavaScript / Sémantique et analyse certifiée de JavaScript

Bodin, Martin 25 November 2016 (has links)
JavaScript est un langage de programmation maintenant très utilisé - y compris dans des domaines où la sécurité est importante. Il est donc important de permettre de vérifier la qualité des logiciels écrit en JavaScript. Cette thèse explore l'approche de la preuve formelle, visant à donner une preuve mathématique qu'un programme donné se comporte comme prévu. Pour construire cette preuve, nous utilisons un assistant de preuve tel que Coq - un programme de confiance permettant de vérifier nos preuves formelles. Pour pouvoir énoncer qu'un programme JavaScript se comporte correctement, nous avons tout d'abord besoin d'une sémantique du langage JavaScript. Cette thèse s'est donc inscrite dans le projet JSCert visant à produire une sémantique formelle pour le langage JavaScript. Devant la taille de la sémantique de JavaScript, il est important de savoir comment on peut lui faire confiance : une faute de frappe peut compromettre toute la sémantique. Pour pouvoir faire confiance à JSCert, nous nous sommes appuyés sur deux sources de confiance. D'une part, JSCert a été conçue pour être très similaire à la spécification officielle de JavaScript, le standard ECMAScript : ils utilisent les mêmes structures de donnée, et il est possible d'associer chaque règle de réduction dans JSCert à une ligne d'ECMAScript. D'autre part, nous avons défini et prouvé relativement à JSCert un interpréteur nommé JSRef. Nous avons aussi pu lancer JSRef sur les suites de test de JavaScript. La sémantique de JSCert n'est pas la première sémantique formelle pour le JavaScript, mais c'est la première à proposer deux manières distinctes pour relier la sémantique formelle au langage JavaScript : en ayant une sémantique très similaire à la spécification officielle, et en ayant testé cette sémantique pour la comparer aux autres interpréteurs. Plutôt que de prouver indépendamment que chaque programme JavaScript s'exécute comme prévu, nous analysons ses programmes par interprétation abstraite. Cela consiste à interpréter la sémantique d'un langage avec des domaines abstraits. Par exemple la valeur concrète 1 pourra être remplacée par la valeur abstraite +. L'interprétation abstraite se compose en deux étapes : d'abord une sémantique abstraite est construite et prouvée correcte vis à vis de sa sémantique concrète, puis des analyseurs sont construits selon cette sémantique abstraite. Nous ne nous intéresserons qu'à la première étape dans cette thèse. La sémantique de JSCert est immense - plus de huit cent règles de réduction. La construction d'une sémantique abstraite traditionnelle ne passent pas à l'échelle face à de telles tailles. Nous avons donc conçu une nouvelle manière de construire des sémantiques abstraites à partir de sémantiques concrètes. Notre méthode se base sur une analyse précise de la structure des règles de réduction et vise à minimiser l'effort de preuve. Nous avons appliqué cette méthode sur plusieurs langages. Dans le but d'appliquer notre approche sur JavaScript, nous avons construit un domaine basé sur la logique de séparation. Cette logique requiert de nombreuses adaptations pour pouvoir s'appliquer dans le cadre de l'interprétation abstraite. Cette thèse en étudie les interactions et propose une nouvelle approche pour les solutionner dans le cadre construit précédemment. Nos domaines, bien qu'assez simple par rapport au modèle mémoire de JavaScript, semblent permettre la preuve d'analyseurs déjà existant. Les contributions de cette thèse sont donc triples : une sémantique formelle de confiance pour le langage JavaScript, un formalisme générique pour construire des sémantiques abstraites, et un domaine non trivial pour ce formalisme. / JavaScript is a trending programming language. It is not used in applications in which security may be an important issue. It thus becomes important to be able to control the quality of softwares written in JavaScript. This thesis explores a formal proof approach, which aims at giving a mathematical proof that a given program behaves as expected. To build this proof, we use proof assistants such as Coq—a trusted program enabling to check formal proofs. To state that a JavaScript program is behaving as expected, we first need a semantics of the JavaScript language. This thesis is thus part of the JSCert project, whose aim it to prove a formal semantics for JavaScript. Because of the size of JavaScript's semantics, it is crucial to know how it can be trusted: a typing mistake could compromise the whole semantics. To trust JSCert, we based ourselves on two trust sources. On one hand, JSCert has been designed to be the most similar it can be from the official JavaScript specification, the ECMAScript standard: they use the same data structures, and it is possible to relate each derivation rule in JSCert to a line of ECMAScript. On the other hand, we defined and proved correct with respect to JSCert an interpreter named JSRef. We have been able to run JSRef on JavaScript test suites. The JSCert semantics is not the first formal semantics of JavaScript, but it is the first to propose two distinct ways to relate the formal semantics to the JavaScript language: by having a semantics close to the official specification, and by testing this semantics and comparing it to other interpreters. Instead of independently proving that each JavaScript program behaves as expected, we chose to analyse programs using abstract interpretation. It consists of interpreting the semantics of a programming language with abstract domains. For instance, the concrete value 1 can be replaced by the abstract value +. Abstract interpretation is split into two steps : first, an abstract semantics is built and proven correct with respect to its concrete semantics, then, analysers are built from this abstract semantics. We only focus on the first step in this thesis. The JSCert semantics is huge - more than height hundred derivation rules. Building an abstract semantics using traditional techniques does not scale towards such sizes. We thus designed a new way to build abstract semantics from concrete semantics. Our approach is based on a careful analysis on the structure of derivation rules. It aims at minimising the proof effort needed to build an abstract semantics. We applied our method on several languages. With the goal of applying our approach to JavaScript, we built a domain based on separation logic. This logic require several adaptations to be able to apply in the context of abstract interpretation. This thesis precisely studies these interactions and introduces a new approach to solve them in our abstract interpretation framework. Our domains, although very simple compared to the memory model of JavaScript, seems to enable the proof of already existing analysers. This thesis has thus three main contributions : a trusted formal semantics for the JavaScript, a generic framework to build abstract semantics, and a non-trivial domain for this formalism.
5

EVA, an Evolved Value Analysis for Frama-C : structuring an abstract interpreter through value and state abstractions / Structurer un interpréteur abstrait autour d'abstractions d'états et de valeurs : EVA, une analyse de valeurs évoluée pour Frama-C

Bühler, David 15 March 2017 (has links)
Cette thèse propose un nouveau cadre pour la composition de domaines abstraits. L'idée principale en est l'organisation d'une sémantique abstraite suivant la distinction usuelle entre expressions et instructions, en cours dans la plupart des langages impératifs. La définition d'une sémantique abstraite peut alors se diviser entre abstractions de valeurs et abstractions d'états (ou domaine abstrait). Les abstractions de valeurs représentent les valeurs possibles d'une expression en un point donné, et assurent l'interprétation de la sémantique des expressions. Les abstractions d'états représentent les états machines qui peuvent se produire lors de l'exécution d'un programme, et permettent d'interpréter la sémantique des instructions. De ce choix de conception découle naturellement un élégant système de communication entre abstractions. Lors de l'interprétation d'une instruction, les abstractions d'états peuvent échanger des informations au moyen d'abstractions de valeurs, qui expriment des propriétés à propos des expressions. Les valeurs forment donc une interface de communication entre états abstraits, mais sont également des éléments canoniques de l'interprétation abstraite. Ils peuvent donc eux-même être combinés par les moyens existants de composition d'abstractions, permettant encore davantage d'interactions entre les composants des sémantiques abstraites. Cette thèse explore les possibilités offertes par cette nouvelle architecture des sémantiques abstraites. Nous décrivons en particulier des stratégies efficaces pour le calcul d'abstractions de valeurs précises à partir des propriétés inférées par les domaines, et nous illustrons les différentes possibilités d'interactions que ce système offre. L'architecture que nous proposons inclue également une collaboration directe des abstractions pour l'émission des alarmes qui signalent les erreurs possibles du programme analysé. Nous proposons également un mécanisme permettant d'interagir avec les composants d'une combinaison générique de types OCaml. Nous utilisons des GADT pour encoder la structure interne d'une combinaison, et construisons automatiquement les fonctions d'injection et de projection entre le produit et ses composants. Cette fonctionnalité permet d'établir une communication directe entre les différentes abstractions d'un interpréteur abstrait. Enfin, une dernière contribution de cette thèse est l'extension automatique de domaines abstraits à l'aide de prédicats logiques qui évitent les pertes d'information aux points de jonction. De fait, lorsque plusieurs chemins d'exécution se rejoignent, un domaine abstrait doit représenter les comportements possibles de chacun des chemins, ce qui engendre souvent des pertes de précision. Pour remédier à cette limitation, nous proposons de propager un ensemble d'états abstraits, munis chacun d'un prédicat qui indique sous quelle condition l'état est valable. Contrairement à d'autres approches, notre analyse ne maintient pas une stricte partition des états abstraits, car les prédicats utilisés ne sont pas mutuellement exclusifs. Cette particularité rend possible des optimisations cruciales pour le passage à l'échelle de cette technique, confirmée par nos résultats expérimentaux sur un programme industriel généré. L'ensemble du système de composition des abstractions proposé dans cette thèse a été mis en œuvre dans EVA, la nouvelle version de l'interpréteur abstrait de Frama-C. EVA a été spécifiquement conçu pour faciliter l'introduction de nouvelles abstractions et permettre des interactions riches entre ces abstractions. Grâce à son architecture modulaire et extensible, cinq nouveaux domaines abstraits ont pu être introduit dans l'analyseur en moins d'un an, améliorant ainsi tant ses capacités que sa précision. / This thesis proposes a new framework for the combination of multiple domains in the abstract interpretation theory. Its core concept is the structuring of the abstract semantics by following the usual distinction between expressions and statements. This can be achieved by a convenient architecture where abstractions are separated in two layers: value abstractions, in charge of the expression semantics, and state abstractions —or abstract domains—, in charge of the statement semantics. This design leads naturally to an elegant communication system where the abstract domains, when interpreting a statement, interact and exchange information through value abstractions, that express properties about expressions. While the values form the communication interface between domains, they are also standard elements of the abstract interpretation framework. The communication system is thus embedded in the abstract semantics, and the usual tools of abstract interpretation apply naturally to value abstractions. For instance, different kinds of value abstractions can be composed through the existing methods of combination of abstractions, enabling even further interaction between the components of the abstract semantics. This thesis explores the possibilities offered by this framework. We discuss efficient strategies to compute precise value abstractions from the information inferred by abstract domains, and illustrate the means of communication between different state abstractions. Our architecture also features a direct collaboration for the emission of alarms that report the possible errors of a program. We also proposes a mechanism to enable interacting with the components of a modular combination of OCaml types. We use GADT to encode the inner shape of a combination, and automatically build injection and projection functions between a product of datatypes and its components. This allows direct communications between the abstractions of an abstract interpreter. Finally, a last contribution of this thesis is the automatic extension of abstract domains to track sets of disjunctive abstract states, each one being qualified with a predicate for which the state holds. This enhances the precision of an abstract semantics at join points, when several possible paths of a program execution meet. At these points, predicates preserve the information usually lost by the merge of abstract states. Unlike other approaches, the analysis does not maintain a strict partition of the abstract states, as the predicates we use are not mutually exclusive. This design enables some optimizations that are crucial for scalability, as confirmed by our experimental results on an industrial, generated program. The general system of abstractions combination has been implemented within EVA, the new version of the abstract interpreter provided by the Frama-C platform. Thus, Eva enjoys a modular and extensible architecture designed to facilitate the introduction of new abstractions and to enable rich interactions between them. Thanks to this work, five new domains from the literature have been implemented in less than a year, enhancing the scope and the precision of the analyzer.
6

Low-cost memory analyses for efficient compilers / Analyses de mémoire à bas cout pour des compilateurs efficaces

Maalej Kammoun, Maroua 26 September 2017 (has links)
La rapidité, la consommation énergétique et l'efficacité des systèmes logiciels et matériels sont devenues les préoccupations majeures de la communauté informatique de nos jours. Gérer de manière correcte et efficace les problématiques mémoire est essentiel pour le développement des programmes de grande tailles sur des architectures de plus en plus complexes. Dans ce contexte, cette thèse contribue aux domaines de l'analyse mémoire et de la compilation tant sur les aspects théoriques que sur les aspects pratiques et expérimentaux. Outre l'étude approfondie de l'état de l'art des analyses mémoire et des différentes limitations qu'elles montrent, notre contribution réside dans la conception et l'évaluation de nouvelles analyses qui remédient au manque de précision des techniques publiées et implémentées. Nous nous sommes principalement attachés à améliorer l'analyse de pointeurs appartenant à une même structure de données, afin de lever une des limitations majeures des compilateurs actuels. Nous développons nos analyses dans le cadre général de l'interprétation abstraite « non dense ». Ce choix est motivé par les aspects de correction et d'efficacité : deux critères requis pour une intégration facile dans un compilateur. La première analyse que nous concevons est basée sur l'analyse d'intervalles des variables entières ; elle utilise le fait que deux pointeurs définis à l'aide d'un même pointeur de base n'aliasent pas si les valeurs possibles des décalages sont disjointes. La seconde analyse que nous développons est inspirée du domaine abstrait des Pentagones ; elle génère des relations d'ordre strict entre des paires de pointeurs comparables. Enfin, nous combinons et enrichissons les deux analyses précédentes dans un cadre plus général. Ces analyses ont été implémentées dans le compilateur LLVM. Nous expérimentons et évaluons leurs performances, et les comparons aux implémentations disponibles selon deux métriques : le nombre de paires de pointeurs pour lesquelles nous inférons le non-aliasing et les optimisations rendues possibles par nos analyses / This thesis was motivated by the emergence of massively parallel processing and supercomputingthat tend to make computer programming extremely performing. Speedup, the power consump-tion, and the efficiency of both software and hardware are nowadays the main concerns of theinformation systems community. Handling memory in a correct and efficient way is a step towardless complex and more performing programs and architectures. This thesis falls into this contextand contributes to memory analysis and compilation fields in both theoretical and experimentalaspects.Besides the deep study of the current state-of-the-art of memory analyses and their limitations,our theoretical results stand in designing new algorithms to recover part of the imprecisionthat published techniques still show. Among the present limitations, we focus our research onthe pointer arithmetic to disambiguate pointers within the same data structure. We develop ouranalyses in the abstract interpretation framework. The key idea behind this choice is correctness,and scalability: two requisite criteria for analyses to be embedded to the compiler construction.The first alias analysis we design is based on the range lattice of integer variables. Given a pair ofpointers defined from a common base pointer, they are disjoint if their offsets cannot have valuesthat intersect at runtime. The second pointer analysis we develop is inspired from the Pentagonabstract domain. We conclude that two pointers do not alias whenever we are able to build astrict relation between them, valid at program points where the two variables are simultaneouslyalive. In a third algorithm we design, we combine both the first and second analysis, and enhancethem with a coarse grained but efficient analysis to deal with non related pointers.We implement these analyses on top of the LLVM compiler. We experiment and evaluate theirperformance based on two metrics: the number of disambiguated pairs of pointers compared tocommon analyses of the compiler, and the optimizations further enabled thanks to the extraprecision they introduce
7

Analyse statique de programmes manipulant des tableaux / Analysis of programs using arrays

Perrelle, Valentin 21 February 2013 (has links)
L’analyse statique de programmes est un domaine crucial en compilation, en optimisation, et en validation de logiciels. Les structures de données complexes (tableaux, listes, graphes...), omniprésentes dans les programmes, posent des problèmes difficiles, du fait qu’elles représentent des ensembles de données de taille importante ou inconnue, et que l’adressage des données dans ces ensembles est calculé (indexation, indirection). La plupart des travaux sur l’analyse des structures de données concernent la vérification de la correction des accès aux données (vérification que les indices d’un tableau sont dans les bornes, que les pointeurs ne sont pas nuls, “shape analysis”). L’analyse du contenu des structures de données est encore peu abordée. A Verimag, ce domaine a été abordé récemment, et a donné lieu à de premiers résultats sur l’analyse de tableaux unidimensionnels. Une méthode d’analyse de programmes simples a été proposée [1], qui permet de découvrir des propriétés des contenus de tableaux, comme par exemple que le résultat d’un programme de tri est bien un tableau trié. Un autre type de propriétés, dites “non positionnelles” a aussi été considéré [2], qui concerne le contenu global d’un tableau, indépendamment de son rangement: par exemple, on montre que le résultat d’un tri est une permutation du tableau initial. Ces premiers résultats sont très encourageants, mais encore embryonnaires. L’objectif du travail de thèse proposé est de les étendre dans plusieurs directions. Notre analyse de propriétés positionnelles est capable de découvrir des relations point- à-point entre des “tranches” de tableaux (ensembles de cellules consécutives). Les extensions envisagées concernent les tableaux multidimensionnels, les ensembles de cellules non nécessairement consécutives, et les structures de données plus générales. Concernant les propriétés non positionnelles, les premiers résultats sont limités aux égalités de contenus de tableaux. Ils doivent être étendus à des relations plus complexes (inclusions, sommes disjointes...) et à d’autres structures de données. Ce travail prend place dans le projet ASOPT (“Analyse statique et optimisation”), accepté dans le programme Arpège de l’ANR en 2008. Références : [1] N. Halbwachs, M. Péron. Discovering properties about arrays in simple programs. ACM Conference on Programming Language Design and Implementation, PLDI 2008. Tucson (Az.), juin 2008. [2] V. Perrelle. Analyse statique du contenu de tableaux, propriétés non positionnelles. Rapport de M2R, Master Parisien de Recherche en Informatique, septembre 2008. / Static analysis is key area in compilation, optimization and software validation. The complex data structures (arrays, dynamic lists, graphs...) are ubiquitous in programs, and can be challenging, because they can be large or of unbounded size and accesses are computed. (through indexing or indirections). Whereas the verification of the validity of the array accesses was one of the initial motivations of abstract interpretation, the discovery of properties about array contents was only adressed recently. Most of the analyses of array contents are based on a partitioning of the arrays. Then, they try to discover properties about each fragment of this partition. The choice of this partition is a difficult problem and each method have its flaw. Moreover, classical representations of array partitions induce an exponential complexity for these analyzes. In this thesis, we generalize the concept of array partitioning into the concept of "fragmentation" which allow overlapping fragments, handling potentially empty fragments and selecting specialized relations. On the other hand, we propose an abstraction of these fragmentations in terms of graphs called "slices diagrams" as well as the operations to manipulate them and ensuring a polynomial complexity. Finally, we propose a new criterion to compute a semantic fragmentation inspired by the existing ones which attempt to correct their flaws. These methods have been implemented in a static analyzer. Experimentations shows that the analyzer can efficiently and precisly prove some challenging exemples in the field of static analysis of programs manipulating arrays.
8

Techniques for formal modelling and verification on dynamic memory allocators / Techniques de modélisation et de vérification formelles des allocateurs de mémoire dynamiques

Fang, Bin 10 September 2018 (has links)
Cette thèse est une contribution à la spécification et à la vérification formelles des allocateurs de mémoire dynamiques séquentiels (SDMA, en abrégé), qui sont des composants clés des systèmes d'exploitation ou de certaines bibliothèques logiciel. Les SDMA gèrent la partie tas de la mémoire des processus. Leurs implémentations utilisent à la fois des structures de données complexes et des opérations de bas niveau. Cette thèse se concentre sur les SDMA qui utilisent des structures de données de type liste pour gérer les blocs du tas disponibles pour l'allocation (SDMA à liste).La première partie de la thèse montre comment obtenir des spécifications formelles de SDMA à liste en utilisant une approche basée sur le raffinement. La thèse définit une hiérarchie de modèles classés par la relation de raffinement qui capture une grande variété de techniques et de politiques employées par le implémentations réelles de SDMA. Cette hiérarchie forme une théorie algorithmique pour les SDMA à liste et pourrait être étendue avec d'autres politiques. Les spécifications formelles sont écrites en Event-B et les raffinements ont été prouvés en utilisant la plateforme Rodin. La thèse étudie diverses applications des spécifications formelles obtenues: le test basé sur des modèles, la génération de code et la vérification.La deuxième partie de la thèse définit une technique de vérification basée sur l'interprétation abstraite. Cette technique peut inférer des invariants précis des implémentations existantes de SDMA. Pour cela, la thèse définit un domaine abstrait dont les valeurs representent des ensembles d'états du SDMA. Le domaine abstrait est basé sur un fragment de la logique de séparation, appelé SLMA. Ce fragment capture les propriétés liées à la forme et au contenu des structures de données utilisées par le SDMA pour gérer le tas. Le domaine abstrait est défini comme un produit spécifique d'un domaine abstrait pour graphes du tas avec un domaine abstrait pour des sequences finies d'adresses mémoire. Pour obtenir des valueurs abstraites compactes, la thèse propose une organisation hiérarchique des valeurs abstraites: un premier niveau abstrait la liste de tous les blocs mémoire, alors qu'un second niveau ne sélectionne que les blocs disponibles pour l’allocation. La thèse définit les transformateurs des valeurs abstraites qui capturent la sémantique des instructions utilisées dans les implémentations des SDMA. Un prototype d'implémentation de ce domaine abstrait a été utilisé pour analyser des implémentations simples de SDMA. / The first part of the thesis demonstrates how to obtain formal specifications of free-list SDMA using a refinement-based approach. The thesis defines a hierarchy of models ranked by the refinement relation that capture a large variety of techniques and policies employed by real-work SDMA. This hierarchy forms an algorithm theory for the free-list SDMA and could be extended with other policies. The formal specifications are written in Event-B and the refinements have been proved using the Rodin platform. The thesis investigates applications of the formal specifications obtained, such as model-based testing, code generation and verification.The second part of the thesis defines a technique for inferring precise invariants of existing implementations of SDMA based abstract interpretation. For this, the thesis defines an abstract domain representing sets of states of the SDMA. The abstract domain is based on a fragment of Separation Logic, called SLMA. This fragment captures properties related with the shape and the content of data structures used by the SDMA to manage the heap. The abstract domain is defined as a specific product of an abstract domain for heap shapes with an abstract domain for finite arrays of locations. To obtain compact elements of this abstract domain, the thesis proposes an hierarchical organisation of the abstract values: a first level abstracts the list of all chunks while a second level selects only the chunks available for allocation. The thesis defines transformers of the abstract values that soundly capture the semantics of statements used in SDMA implementations. A prototype implementation of this abstract domain has been used to analyse simple implementations of SDMA
9

Simulation abstraite : une analyse statique de modèles Simulink

Chapoutot, Alexandre 08 December 2008 (has links) (PDF)
La conception de systèmes embarqués nécessite de plus en plus l'utilisation d'outils logiciels afin de contenir la complexité croissante de ceux-ci. Les deux principaux outils industriels dans ce domaine sont Simulink et Lustre/Scade. Ces deux outils possèdent de nombreuses fonctionnalités comme un moteur de simulations, des générateurs de tests ou de code. Cependant, Simulink est, dans la majorité des cas, utilisé pour la conception de systèmes embarqués et ceci parce qu'il a une expressivité plus importante. Il est capable de modéliser et de simuler des systèmes à temps continu, à temps discret et un mélange des deux, c'est-à-dire des systèmes hybrides. Pour la conception des systèmes embarqués, Simulink permet de modéliser l'environnement physique et le logiciel embarqué dans un même formalisme. L'application des méthodes formelles sur de telles spécifications est un défi industriel et scientifique important pour la validation des logiciels embarqués. De plus, l'utilisation de méthodes formelles, au plus tôt dans le cycle de développement, est un challenge essentiel dans l'industrie afin de réduire les coûts liés à la correction de bogues.<br /><br />Dans cette thèse, nous définissons une analyse statique par interprétation abstraite de modèles Simulink. Nous appelons cette analyse Simulation Abstraite. L'objectif de la Simulation Abstraite est de fournir un critère de correction des comportements numériques des exécutions des modèles Simulink. Ces simulations sont souvent utilisées pour valider les systèmes modélisés, mais elles sont plus proches de l'activité de tests que celle de la preuve. En conséquence, elles ne permettent pas de valider vis-à-vis des spécifications un système modélisé avec Simulink. La Simulation Abstraite fournit un critère de correction dans le sens que les comportements des modèles Simulink représentent au mieux les comportements du monde réel.<br /><br />Nous supposons que le modèle mathématique, représenté par un modèle Simulink, est correcte vis-à-vis du monde réel. Notre objectif est de calculer automatiquement et conjointement une sur-approximation des comportements mathématiques et des comportements issus de la simulation numérique pour une plage d'entrées possibles. Nous sommes ainsi capable d'estimer l'ensemble des imprécisions introduit par la simulation numérique, c'est-à-dire les erreurs d'arrondi ou les erreurs de troncature liées, par exemple, aux capteurs. Le critère de correction des modèles à temps continu est obtenu en évaluant la distance séparant les résultats des méthodes d'intégration numérique, utilisées par le moteur de simulations, des résultats obtenus par une méthode d'intégration numérique garantie. Le critère de correction des modèles à temps discret est donné par l'utilisation du domaine numérique abstrait des nombres flottants avec erreurs différentiées. Ce nouveau domaine numérique est issu de la combinaison du domaine des flottants avec erreurs et la méthode de différentiation automatique permettant d'avoir une meilleure abstraction des erreurs. Nous définissons également une abstraction d'un domaine des séquences utilisant les partitions d'un ensemble. Nous sommes ainsi en mesure de représenter des simulations infinies d'une manière finie. L'ensemble de ces domaines permet alors d'estimer les erreurs introduites par les traitements numériques présents lors des simulations. Nous obtenons alors une méthode de validation des comportements numériques des systèmes embarqués modélisés en Simulink.
10

Analyse de programmes probabilistes par interprétation abstraite

Monniaux, David 21 November 2001 (has links) (PDF)
L'étude de programmes probabilistes intéresse plusieurs domaines de l'informatique : les réseaux, l'embarqué, ou encore la compilation optimisée. C'est tâche malaisée, en raison de l'indécidabilité des propriétés sur les programmes déterministes à états infinis, en plus des difficultés provenant des aspects probabilistes.<br /><br />Dans cette thèse, nous proposons un langage de formules permettant de spécifier des propriétés de traces de systèmes de transition probabilistes et non-déterministes, englobant celles spécifiables par des automates de Büchi déterministes. Ces propriétés sont en général indécidables sur des processus infinis.<br /><br />Ce langage a à la fois une sémantique concrète en termes d'ensembles de traces et une sémantique abstraite en termes de fonctions mesurables. Nous appliquons ensuite des techniques d'interprétation abstraite pour calculer un majorant de la probabilité dans le pire cas de la propriété étudiée et donnons une amélioration de cette technique lorsque l'espace d'états est partitionné, par exemple selon les points de programme. Nous proposons deux domaines abstraits convenant pour cette analyse, l'un paramétré par un domaine abstrait non probabiliste, l'autre modélisant les gaussiennes étendues.<br /><br />Il est également possible d'obtenir de tels majorants par des calculs propageant les mesures de probabilité en avant. Nous donnons une méthode d'interprétation abstraite pour analyser une classe de formules de cette façon et proposons deux domaines abstraits adaptés à ce type d'analyse, l'un paramétré par un domaine abstrait non probabiliste, l'autre modélisant les queues sous-exponentielles. Ce dernier permet de prouver la terminaison probabiliste de programmes.<br /><br />Les méthodes décrites ci-dessus sont symboliques et ne tirent pas parti des propriétés statistiques des probabilités. Nous proposons d'autre part une méthode de Monte-Carlo abstrait, utilisant des interpréteurs abstraits randomisés.

Page generated in 0.1893 seconds