Bouissou, Olivier (2008) Analyse statique par interprétation abstraite de systèmes hybrides. PhD thesis MeASI (CEA Saclay), MeASI (CEA Saclay), EP/X p.185.

Alternative Locations: http://www.imprimerie.polytechnique.fr/Theses/Files/Bouissou.pdf

Abstract

Pour améliorer la précision des méthodes d’analyse statique des programmes critiques embarqués, on considère en plus du programme lui-même l’environnement physique dans lequel le programme est exécuté. Nous présentons une extension des langages de programmation impératifs décrivant à la fois le programme, l’environnement extérieur et leurs interactions. Nous donnons à l’ensemble (programme plus environnement physique) une sémantique dénotationnelle qui reste très proche de celle des langages impératifs. Les solutions des équations différentielles modélisant l’environnement sont exprimées comme le plus petit point fixe d’un opérateur monotone dans un CPO, et nous montrons que les itérées de Kleene convergent vers ce point fixe. Nous donnons aussi une méthode d’analyse statique de ces systèmes hybrides. Après avoir construit un recouvrement de l’espace des variables d’entrée via une analyse par intervalle, ce qui permet d’abstraire l’impact du programme sur son environnement, nous utilisons une méthode d’intégration garantie pour obtenir une surapproximation de l’évolution continue. Un analyseur prototype a été développé et les tests sur les exemples classiques de systèmes hybrides montrent de bons résultats. Enfin, nous présentons une méthode d’intégration garantie nommée GRKLib qui se fonde sur un schéma d’intégration numérique non garanti et nous calculons, grâce à l’arithmétique d’intervalles, une surapproximation de l’erreur globale. Cette erreur s’exprime comme la somme de trois termes calculés séparément et des techniques spécifiques permettent de les réduire. Une librairie C++ a été développée, et les résultats présentés dans cette thèse sont prometteurs.

References

To increase the accuracy of static analysis tools for highly critical embedded programs, we consider, in addition to the program itself, the physical environment in which the program is executed. We present an extension of imperative programming languages that describe the program, its physical environment and the interactions between both. We give to the system made of a program and its environment a denotational semantics that remains very close to that of imperative programming languages. In particular, we express the solution of the differential equations representing the environment as the fixpoint of a monotone map on a CPO, and we show that Kleene’s iterates converge towards this fixpoint. We also provide a static analysis method for such hybrid systems. We first abstract the impact of the program on its environment by building a paving of the input variables space. We use interval analysis for that. Then, we use a guaranteed integration method to obtain an overapproximation of the continuous evolution. A prototype analyser was developed and showed to have good results on the classical hybrid systems benchmarks. Finally, we present a guaranteed integration algorithm named GRKLib. It is based on a numerical, non guaranteed integration scheme et we compute, using interval arithmetics, an overapproximation of the global error. This error is expressed as the sum of three terms, each of them being computed separately using specific techniques to keep it small. A C++ library was developed and the results shown in this thesis are promising.

Table of content

Chapitre 1 : Introduction

Partie I : Etat de l'art

Chapitre 2 : Analyse de la partie discrète, interprétation abstraite

Chapitre 3 : Analyse de la partie continue, intégration garantie

Chapitre 4 : Systèmes hybrides

Partie II : Concret

Chapitre 5 : Un modèle et une sémantique pour les programmes hybrides

Partie III : Abstrait

Chapitre 6 : Abstraction de la partie continue

Chapitre 7 : Abstraction globale

Chapitre 8 : Conclusion et perspectives

Statistiques de consultation

Repository Staff Only: edit this item