Analyse statique par interprétation abstraite de systèmes hybrides.

The power and efficiency of abstract interpretation based static analysis methods for the verification of safety critical embedded software is no longer to be outlined. However, the precision of the analysers needs now to be reinforced. The use of ever more sophisticated relational abstract domains make it possible to reduce the overapproximation that limits the power of simpler domains, but the precision of the latest analysers is still constrained by the precision of the input values. These are given by a sensor that measures some physical phenomena, and they are generally overapproximated by an interval. In order to deal better with these continuous inputs, one may analyse, in addition to the program itself, the physical environment in which the program is executed. In this way, we obtain a more complex system which has both a discrete dynamics (the program) and a continuous one (the environment). Such hybrid systems are generally studied using extensions of finite automata or process calculi that introduce a continuous dynamics. The use of model-checking techniques still suffers from a combinatorial explosion that prohibits the use of such models for the analysis of large safety critical embedded programs. The first contribution of this thesis is to provide an extension of imperative programming lan- guages that describes both the program, the external environment and the interactions between both. The physical environment is described as a set of differential equations, each of them re- presenting a continuous mode. The interactions between the program and the environment are modeled using two extra keywords that represent the effect of sensors and actuators. A denota- tional semantics is given to the whole system (the program and the environment together). This semantics remains very close to the standard denotational semantics of imperative languages. The main difficulty was to define a semantics for the continuous part of the system : we express the solutions of differential equations as the fixpoint of a monotone operator in a CPO, and we show that Kleene's iteration converges towards this fixpoint. The second contribution is an abstract interpretation based static analysis of these hybrid systems. Our method has two stages. First, under some assumptions on the program to be ana- lysed, a partitioning of the space of the input variables is built. For that, we combine a forward reachability method with an interval based analysis. In this way, we obtain an abstraction of the impact of the program on the continuous evolution : the continuous space is divided into zones in which we know that an actuator will be activated. The second stage of the analysis use this partitioning and a guaranteed integration of differential equations algorithm in order to build a safe overaproximation of the continuous evolution. A prototype analyser using these techniques was implemented and the first results on examples of hybrid systems from the literature show good results. Finally, the third contribution of this thesis is a new guaranteed integration algorithm named GRKLib. Unlike existing methods, GRKLib is based on a non-validated, numerical integration scheme (we chose an order 5 Runge-Kutta method, but any other algorithm works). The global error made during the numerical integration is then computed using interval arithmetic. This error is expressed as the sum of three terms : the one-step error, the propagation error and the computation error due to the use of floating point numbers. Each term is computed separately and advanced techniques are used in order to reduce them and control the integration step size so that the growth of the global error is limited. A C++ library implementing these concepts was developed and the results presented in this thesis are very promising.Si l'interet et l'efficacite des methodes d'analyse statique par interpretation abstraite pour la verification des programmes critiques embarques ne sont plus a demontrer, il est maintenant necessaire d'obtenir des methodes les plus precises possibles. Si l'utilisation de domaines abstraits relationnels de plus en plus elabores permet de diminuer la surapproximation dont souffre les domaines les plus simples, les analyses actuelles souffrent toujours d'une mauvais prise en compte des entrees du programme. Ces entrees sont fournies par un capteur qui mesure une grandeur physique, et sont generalement surapproximees par un intervalle. Une piste d'etude recente pour mieux gerer ces entrees continues consiste a etudier, outre le programme lui-meme, l'environnement physique dans lequel il est execute. On obtient ainsi un systeme plus complexe comprenant une dynamique discrete (le programme) et une dynamique continue (l'environnement). L'etude de tels systemes hybrides repose actuellement essentiellement sur des extensions des automates a etats finis et des algebres de processus introduisant une dynamique continue. L'analyse de ces systemes par des techniques de model-checking souffre encore d'une explosion combinatoire excluant leur utilisation pour les logiciels embarques critiques les plus gros. La premiere contribution de cette these est une extension des langages de programmation imperatifs permettant de d´ecrire a la fois le programme, l'environnement exterieur et les interactions entre le programme et l'environnement. L'environnement physique est d´ecrit par un ensemble d'equations differentielles representant chacune un mode continu, et les interactions entre le programme et l'exterieur sont modelises par deux mots cles representant les capteurs et actionneurs. Nous donnons a l'ensemble (programme plus environnement physique) une semantique denotationnelle qui reste tres proche de celle definie pour les langages imperatifs classiques. La difficulte majeure dans la construction de cette semantique a ete de definir une semantique pour la partie continue : les solutions des equations diff´erentielles sont exprimees comme le plus petit point fixe d'un operateur monotone dans un CPO, et nous montrons que les iterees de Kleene convergent vers ce point fixe. La seconde contribution est une methode d'analyse statique par interpretation abstraite de ces systemes hybrides. Cette methode fonctionne en deux temps. Tout d'abord, sous certaines restrictions portant sur le programme a analyser, on construit un recouvrement de l'espace des variables d'entree via une analyse par intervalle couplee a une analyse d'atteignabilite en avant. On obtient ainsi une abstraction de l'impact qu'a le programme sur l'evolution continue : l'espace d'entree du programme est d´coupe en zones dans lesquelles on est sur qu'un actionneur sera active. Dans un deuxieme temps, nous utilisons ce recouvrement et une methode d'integration garantie des equations differentielles pour obtenir une surapproximation de l'evolution continue. Un analyseur prototype implementant ces techniques a ete developpe et les tests sur les exemples classiques de systemes hybrides montrent de bons resultats. Enfin, la troisieme contribution de cette these est une nouvelle methode d'integration garantie nommee GRKLib. Contrairement aux methodes existantes, GRKLib se fonde sur un schema d'integration numerique non garantie (nous avons choisi un schema de Runge-Kutta d'ordre 4, mais n'importe quelle autre convient) et nous calculons, en utilisant l'arithmetique d'intervalles, l'erreur globale commise lors de l'integration numerique. Cette erreur s'exprime comme la somme de trois termes : l'erreur sur un pas, la propagation de l'erreur et l'erreur due aux nombres flottants. Chaque terme est calcule separement et des techniques avancees permettent de les reduire et de controler au mieux le pas d'integration pour limiter l'accroissement de l'erreur globale. Une librairie C++ implementant ces concepts a ete developpee, et les resultats presentes dans cette these sont prometteurs