Abstract FR:

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.