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.
| Identifer | oai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00004412 |
| Date | 23 September 2008 |
| Creators | Bouissou, Olivier |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0022 seconds