Static analysis of control-command systems : floating-point and integer invariants

Un logiciel critique est un logiciel dont le mauvais fonctionnement peut avoir un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens.L'ingénierie logicielle pour les systèmes critiques est particulièrement difficile et combine différentes méthodes pour garantir la qualité des logiciels produits.Parmi celles-ci, les méthodes formelles peuvent être utilisées pour prouver qu'un logiciel respecte ses spécifications.Le travail décrit dans cette thèse s'inscrit dans le contexte de la validation de propriétés de sûreté de programmes critiques, et plus particulièrement des propriétés numériques de logiciels embarqués dans des systèmes de contrôle-commande.La première partie de cette thèse est consacrée aux preuves de stabilité au sens de Lyapunov.Ces preuves s'appuient sur des calculs en nombres réels, et ne sont pas valables pour décrire le comportement d'un programme exécuté sur une plateforme à arithmétique machine.Nous présentons un cadre théorique générique pour adapter les arguments des preuves de stabilité de Lyapunov aux arithmétiques machine.Un outil effectue automatiquement la traduction de la preuve en nombres réels vers une preuve en nombres a virgule flottante.La seconde partie de la thèse porte sur l'analyse des relations affines, en utilisant une interprétation abstraite basée sur l'approximation des valuations associées aux points de contrôle d'un programme par des polyèdres convexes.Nous présentons ALICe, un framework permettant de comparer différentes techniques de génération d'invariants.Il s'accompagne d'une collection de cas de tests tirés de publications sur l'analyse de programmes, et s'interface avec trois outils utilisant différents algorithmes de calcul d'invariants: Aspic, iscc et PIPS.Afin d'affiner les résultats de PIPS, deux techniques de restructuration de code sont introduites, et plusieurs améliorations sont apportées aux algorithmes de génération d'invariants et évaluées à l'aide d'ALICe.A critical software is a software whose malfunction may result in death or serious injury to people, loss or severe damage to equipment or environmental harm.Software engineering for critical systems is particularly difficult, and combines different methods to ensure the quality of produced software.Among them, formal methods can be used to prove that a software obeys its specifications.This thesis falls within the context of the validation of safety properties for critical software, and more specifically, of numerical properties for embedded software in control-command systems.The first part of this thesis deals with Lyapunov stability proofs.These proofs rely on computations with real numbers, and do not accurately describe the behavior of a program run on a platform with machine arithmetic.We introduce a generic, theoretical framework to adapt the arguments of Lyapunov stability proofs to machine arithmetic.A tool automatically translates the proof on real numbers to a proof with floating-point numbers.The second part of the thesis focuses on linear relation analysis, using an abstract interpretation based on the approximation by convex polyhedrons of valuations associated with each control point in a program.We present ALICe, a framework to compare different invariant generation techniques.It comes with a collection of test cases taken from the program analysis literature, and interfaces with three tools, that rely on different algorithms to compute invariants: Aspic, iscc and PIPS.To refine PIPS results, two code restructuring techniques are introduced, and several improvements are made to the invariant generation algorithms and evaluated using ALICe