La conception de systèmes embarqués nécessite de plus en plus l'utilisation d'outils logiciels afin de contenir la complexité croissante de ceux-ci. Les deux principaux outils industriels dans ce domaine sont Simulink et Lustre/Scade. Ces deux outils possèdent de nombreuses fonctionnalités comme un moteur de simulations, des générateurs de tests ou de code. Cependant, Simulink est, dans la majorité des cas, utilisé pour la conception de systèmes embarqués et ceci parce qu'il a une expressivité plus importante. Il est capable de modéliser et de simuler des systèmes à temps continu, à temps discret et un mélange des deux, c'est-à-dire des systèmes hybrides. Pour la conception des systèmes embarqués, Simulink permet de modéliser l'environnement physique et le logiciel embarqué dans un même formalisme. L'application des méthodes formelles sur de telles spécifications est un défi industriel et scientifique important pour la validation des logiciels embarqués. De plus, l'utilisation de méthodes formelles, au plus tôt dans le cycle de développement, est un challenge essentiel dans l'industrie afin de réduire les coûts liés à la correction de bogues.<br /><br />Dans cette thèse, nous définissons une analyse statique par interprétation abstraite de modèles Simulink. Nous appelons cette analyse Simulation Abstraite. L'objectif de la Simulation Abstraite est de fournir un critère de correction des comportements numériques des exécutions des modèles Simulink. Ces simulations sont souvent utilisées pour valider les systèmes modélisés, mais elles sont plus proches de l'activité de tests que celle de la preuve. En conséquence, elles ne permettent pas de valider vis-à-vis des spécifications un système modélisé avec Simulink. La Simulation Abstraite fournit un critère de correction dans le sens que les comportements des modèles Simulink représentent au mieux les comportements du monde réel.<br /><br />Nous supposons que le modèle mathématique, représenté par un modèle Simulink, est correcte vis-à-vis du monde réel. Notre objectif est de calculer automatiquement et conjointement une sur-approximation des comportements mathématiques et des comportements issus de la simulation numérique pour une plage d'entrées possibles. Nous sommes ainsi capable d'estimer l'ensemble des imprécisions introduit par la simulation numérique, c'est-à-dire les erreurs d'arrondi ou les erreurs de troncature liées, par exemple, aux capteurs. Le critère de correction des modèles à temps continu est obtenu en évaluant la distance séparant les résultats des méthodes d'intégration numérique, utilisées par le moteur de simulations, des résultats obtenus par une méthode d'intégration numérique garantie. Le critère de correction des modèles à temps discret est donné par l'utilisation du domaine numérique abstrait des nombres flottants avec erreurs différentiées. Ce nouveau domaine numérique est issu de la combinaison du domaine des flottants avec erreurs et la méthode de différentiation automatique permettant d'avoir une meilleure abstraction des erreurs. Nous définissons également une abstraction d'un domaine des séquences utilisant les partitions d'un ensemble. Nous sommes ainsi en mesure de représenter des simulations infinies d'une manière finie. L'ensemble de ces domaines permet alors d'estimer les erreurs introduites par les traitements numériques présents lors des simulations. Nous obtenons alors une méthode de validation des comportements numériques des systèmes embarqués modélisés en Simulink.

La vérification des programmes est un enjeu majeur pour les applications critiques comme l'aviation, l'aérospatiale ou les systèmes embarqués. Les approches Bounded model checking (e.g., CBMC) et de programmation par contraintes (e.g., CPBPV, …) reposent sur la recherche de contre-exemples qui violent une propriété du programme à vérifier. La recherche de tels contre-exemples peut être très longue et coûteuse lorsque les programmes à vérifier contiennent des calculs en virgule flottante. Ceci est dû en grande partie au fait que les stratégies de recherche existantes ont été conçues pour des domaines finis et, dans une moindre mesure, pour des domaines continus. Dans cette thèse, nous proposons un ensemble de stratégie de recherche dédié à la vérification de programme avec du calcul sur les flottants. Les stratégies proposées pour les choix de variables et de choix de valeur se basent sur des propriétés propres aux flottants. Ces propriétés utilisent des caractéristiques des domaines des variables, ou de la structure des contraintes. Certaines propriétés qui portent sur les domaines des variables sont classiques comme la taille et la cardinalité et d'autres beaucoup plus spécifiques comme la densité. Les notions de taille et cardinalité sont équivalentes sur les entiers, mais ne le sont pas sur les flottants. Ainsi la densité capture une variabilité qui est très spécifique aux flottants dont la moitié se trouve entre [-1,1]. De manière similaire les propriétés qui portent sur la structure des contraintes sont, pour certaines tels que le degré ou le nombre d’occurrences, issues des domaines finis, et pour d’autres beaucoup plus spécifiques, comme l’absorption, et la cancellation; ces deux propriétés capturent des phénomènes qui sont généralement la cause de fortes déviations du programme flottant vis-à-vis son interprétation sur les réels et donc de l’existence même de beaucoup de contre-exemples. Pour chaque propriété, deux stratégies de choix de variables sont proposées. La première choisit la variable qui minimise la propriété, alors que la seconde choisit la variable qui la maximise. Les stratégies de choix de valeurs essaient quant à elles de tirer profit des phénomènes d'absorption et de cancellation. L'évaluation de ces stratégies sur un ensemble de programmes réalistes est très encourageante : ces stratégies sont plus efficaces que les stratégies standards. / Program verification is a major issue for critical applications such as aviation, aerospace or embedded systems. Bounded model checking (e.g., CBMC) and constraint programming (e.g., CPBPV,...) approaches are based on the search for counter-examples that violate a property of the program to verify. The search for such counter-examples can be very time-consuming and costly when the programs to be verified contain floating point calculations. This is largely due to the fact that existing research strategies have been designed for finite domains and, to a lesser extent, for continuous domains. In this thesis, we propose a set of search strategies dedicated to program verification with floating point computation. The proposed strategies for variable and value selection are based on specific floating properties. These properties use characteristics of the variable domains, or the constraint structure. Some properties that focus on the domains of the variables are classic such as size and cardinality and others much more specific like density. The notions of size and cardinality are equivalent on the integers, but not on the floats. Density captures a variability that is very specific to the floats, half of which are between[-1.1]. Similarly, the properties that concern the structure of constraints are, for some such as the degree or number of occurrences, derived from finite domains, and for others much more specific, such as absorption, and cancellation; these two properties capture phenomena that are generally the cause of strong deviations of the floating point program from its interpretation on the reals and hence the existence of many counterexamples. For each property, two variable selection strategies are proposed. The first one chooses the variable that minimizes the property, while the second one chooses the variable that maximizes it. Value choice strategies try to take advantage of the phenomena of absorption and cancellation.

Le tristement célèbre Ecran Bleu de la Mort de Windows introduit bien le problème traité. Ce bug est souvent causé par la non-terminaison d'un pilote matériel : le programme s'exécute infiniment, bloquant ainsi toutes les ressources qu'il s'est approprié pour effectuer ses calculs. Cette thèse développe des techniques qui permettent de décider, préalablement à l'exécution, la terminaison d'un programme donné pour l'ensemble des valeurs possibles de ses paramètres en entrée. En particulier, nous nous intéressons aux programmes qui manipulent des nombres flottants. Ces nombres sont omniprésents dans les processeurs actuels et sont utilisés par pratiquement tous les développeurs informatiques. Pourtant, ils sont souvent mal compris et, de fait, source de bugs. En effet, les calculs flottants sont entachés d'erreurs, inhérentes au fait qu'ils sont effectués avec une mémoire finie. Par exemple, bien que vraie dans les réels, l'égalité 0.2 + 0.3 = 0.5 est fausse dans les flottants. Non gérées correctement, ces erreurs peuvent amener à des évènements catastrophiques, tel l'incident du missile Patriot qui a fait 28 morts. Les théories que nous développons sont illustrées, et mises à l'épreuve par des extraits de codes issus de programmes largement répandus. Notamment, nous avons pu exhiber des bugs de terminaisons dues à des calculs flottants incorrects dans certains paquets de la distribution Ubuntu. / The infamous Blue Screen of Death of Windows appropriately introduces the problem at hand. This bug is often caused by a non-terminating device driver: the program runs infinitely, blocking in the process all the resources it allocated for its calculations. This thesis develops techniques that allow to decide, before runtime,termination of a given program for any possible value ​​of its inputs. In particular, we are interested in programs that manipulate floating-point numbers. These numbers are ubiquitous in current processors andare used by nearly all software developers. Yet, they are often misunderstood and, hence, source of bugs.Indeed, floating-point computations are tainted with errors. This is because they are performed within a finite amount of memory. For example, although true in the reals, the equality 0.2 + 0.3 = 0.5 is false in the floats. Not handled properly, these errors can lead to catastrophic events,such as the Patriot missile incident that killed 28 people. The theories we develop are illustrated, and put to the test, by code snippets taken from widely used programs. Notably, we were able to exhibit termination bugs due toincorrect floating-point computations in some packages of the Ubuntu distribution.