No description available.

Les défaillances des applications embarquées dans les systèmes temps-réel strict peuvent avoir des conséquences graves (catastrophes industrielles, mise en danger de vies humaines). La vérification des contraintes temporelles d'un système temps-réel strict dépend de la connaissance du temps d'exécution pire-cas des tâches constituant l'application embarquée. L'utilisation de processeurs multi-cœurs est l'un des moyens actuellement mis en œuvre afin d'améliorer le niveau de performances des systèmes embarqués. Cependant, la détermination du temps d'exécution pire-cas d'une tâche sur ce type d'architecture est rendue difficile par le partage de certaines ressources par les cœurs, et notamment le bus d'interconnexion permettant l'accès à la mémoire centrale. Ce document propose un nouveau mécanisme d'arbitrage de bus à deux niveaux permettant d'améliorer les performances des ensembles de tâches exécutés tout en garantissant le respect des contraintes temporelles. Les méthodes décrites permettent d'établir un niveau de priorité d'accès au bus optimal pour chacune des tâches exécutées. Elles permettent également de trouver une allocation optimale des tâches aux cœurs lorsqu'il y a plus de tâches à exécuter que de cœurs disponibles. Les résultats expérimentaux montrent une diminution significative des estimations de temps d'exécution pire-cas et de l'utilisation du processeur.

La validation des logiciels est une partie cruciale dans le cycle de leur développement. Deux techniques de vérification et de validation se sont démarquées au cours de ces dernières années : l'analyse statique et l'analyse dynamique. Les points forts et faibles des deux techniques sont complémentaires. Nous présentons dans cette thèse une combinaison originale de ces deux techniques. Dans cette combinaison, l'analyse statique signale les instructions risquant de provoquer des erreurs à l'exécution, par des alarmes dont certaines peuvent être de fausses alarmes, puis l'analyse dynamique (génération de tests) est utilisée pour confirmer ou rejeter ces alarmes. L'objectif de cette thèse est de rendre la recherche d'erreurs automatique, plus précise, et plus efficace en temps. Appliquée à des programmes de grande taille, la génération de tests, peut manquer de temps ou d'espace mémoire avant de confirmer certaines alarmes comme de vraies erreurs ou conclure qu'aucun chemin d'exécution ne peut atteindre l'état d'erreur de certaines alarmes et donc rejeter ces alarmes. Pour surmonter ce problème, nous proposons de réduire la taille du code source par le slicing avant de lancer la génération de tests. Le slicing transforme un programme en un autre programme plus simple, appelé slice, qui est équivalent au programme initial par rapport à certains critères. Quatre utilisations du slicing sont étudiées. La première utilisation est nommée all. Elle consiste à appliquer le slicing une seule fois, le critère de simplification étant l'ensemble de toutes les alarmes du programme qui ont été détectées par l'analyse statique. L'inconvénient de cette utilisation est que la génération de tests peut manquer de temps ou d'espace et les alarmes les plus faciles à classer sont pénalisées par l'analyse d'autres alarmes plus complexes. Dans la deuxième utilisation, nommée each, le slicing est effectué séparément par rapport à chaque alarme. Cependant, la génération de tests est exécutée pour chaque programme et il y a un risque de redondance d'analyse si des alarmes sont incluses dans d'autres slices. Pour pallier ces inconvénients, nous avons étudié les dépendances entre les alarmes et nous avons introduit deux utilisations avancées du slicing, nommées min et smart, qui exploitent ces dépendances. Dans l'utilisation min, le slicing est effectué par rapport à un ensemble minimal de sous-ensembles d'alarmes. Ces sous-ensembles sont choisis en fonction de dépendances entre les alarmes et l'union de ces sous-ensembles couvre l'ensemble de toutes les alarmes. Avec cette utilisation, on a moins de slices qu'avec each, et des slices plus simples qu'avec all. Cependant, l'analyse dynamique de certaines slices peut manquer de temps ou d'espace avant de classer certaines alarmes, tandis que l'analyse dynamique d'une slice éventuellement plus simple permettrait de les classer. L'utilisation smart consiste à appliquer l'utilisation précédente itérativement en réduisant la taille des sous-ensembles quand c'est nécessaire. Lorsqu'une alarme ne peut pas être classée par l'analyse dynamique d'une slice, des slices plus simples sont calculées. Nous prouvons la correction de la méthode proposée. Ces travaux sont implantés dans sante, notre outil qui relie l'outil de génération de tests PathCrawler et la plate-forme d'analyse statique Frama-C. Des expérimentations ont montré, d'une part, que notre combinaison est plus performante que chaque technique utilisée indépendamment et, d'autre part, que la vérification devient plus rapide avec l'utilisation du slicing. De plus, la simplification du programme par le slicing rend les erreurs détectées et les alarmes restantes plus faciles à analyser

Les travaux décrits dans ce manuscrit de thèse s'inscrivent dans le cadre des méthodes formelles pour les langages de spécifications formées d'automates communicants. Ce type de langage est largement utilisé dans les industries de pointe où le niveau de fiabilité requis est élevé (e.g. aéronautique, transports), car ils permettent d'améliorer la précision des spécifications et d'exploiter des outils de simulation, de test ou de vérification qui contribuent à la validation des spécifications. Un frein au passage à l'échelle industrielle de ces méthodes formelles est connu sous le nom de l'explosion combinatoire, qui est due à la fois à la manipulation de larges domaines numériques, et au parallélisme intrinsèque aux spécifications.<br />L'idée que nous proposons consiste à contourner ce phénomène en appliquant des techniques de réduction paramétrée, pouvant être désignées sous le terme anglo-saxon "slicing'', en amont d'une analyse complexe. Cette analyse peut ainsi être effectuée a posteriori sur une spécification réduite, donc potentiellement moins sujette à l'explosion combinatoire. Notre méthode de réduction paramétrée est basée sur des relations de dépendances dans la spécification sous analyse, et est fondée principalement sur les travaux effectués par les communautés de la compilation et du slicing de programmes. Dans cette thèse nous établissons un cadre théorique pour les analyses statiques de spécifications formées d'automates communicants, dans lequel nous définissons formellement les relations de dépendances mentionnées ci-dessus, ainsi que le concept de "tranche" de spécification par rapport à un "critère" de réduction. Ensuite, nous décrivons et démontrons les algorithmes efficaces que nous avons mis au point pour calculer les relations de dépendances et les tranches de spécifications, et enfin nous décrivons notre mise en oeuvre de ces algorithmes dans l'outil "Carver", pour la réduction paramétrée de spécifications formées d'automates communicants.

Les analyses statiques ont pour but de déterminer les propriétés des programmes au moment de la compilation. Contrairement aux analyses dynamiques, le comportement exact du programme ne peut être connu. Par conséquent, on a recours à des approximations pour remédier à ce manque d'information. Malgré ces approximations, les analyses statiques permettent des optimisations et des transformations efficaces pour améliorer les performances des programmes. Parmi les premières analyses du processus d'optimisation figure l'analyse des pointeurs. Son but est d'analyser statiquement un programme en entrée et de fournir en résultat une approximation des emplacements mémoire vers lesquels pointent ses variables pointeurs. Cette analyse est considérée comme l'une des analyses de programmes les plus délicates et l'information qu'elle apporte est très précieuse pour un grand nombre d'autres analyses clientes. En effet, son résultat est nécessaire à d'autres optimisations, comme la propagation de constante, l'élimination du code inutile, le renommage des scalaires ainsi que la parallélisation automatique des programmes. L'analyse des pointeurs est très nécessaire pour l'exploitation du parallélisme présent dans les applications scientifiques écrites en C. Ceci est dû au fait que les tableaux, très présents dans ce type d'applications, sont accédés via les pointeurs. Il devient nécessaire d'analyser les dépendances entre les éléments de tableau dans le but de paralléliser les boucles. Le langage C présente beaucoup de difficultés lors de son analyse par la liberté qu'il offre aux utilisateurs pour gérer et manipuler la mémoire par le biais des pointeurs. Ces difficultés apparaissent par exemple lors de l'accès aux tableaux par pointeurs, l'allocation dynamique (via "malloc") ainsi que les structures de données récursives. L'un des objectifs principaux de cette thèse est de déterminer les emplacements mémoire vers lesquels les pointeurs pointent. Ceci se fait en assurant plusieurs dimensions comme : - la sensibilité au flot de contrôle, c'est-à-dire la mise à jour des informations d'un point programme à un autre ; - la non-sensibilité au contexte, c'est-à-dire l'utilisation de résumés au lieu de l'analyse du corps de la fonction à chaque appel ; - la modélisation des champs pointeurs des structures de données agrégées, dans laquelle chaque champ représente un emplacement mémoire distinct. D'autres aspects sont pris en compte lors de l'analyse des programmes écrits en C comme la précision des emplacements mémoire alloués au niveau du tas, l'arithmétique sur pointeurs ou encore les pointeurs vers tableaux. Notre travail permet l'amélioration des résultats des analyses clientes et en particulier il permet la parallélisation des boucles lorsqu'on accède aux éléments de tableaux via les pointeurs, la détection de code inutile ou le calcul du graphe de dépendances. Il est implémenté dans le compilateur parallélliseur PIPS (Parallélisation Interprocédurale de Programmes Scientifiques) et permet d'analyser, en particulier, les applications scientifiques de traitement du signal tout en assurant une analyse intraprocédurale précise et une analyse interprocédurale efficace via les résumés.

Cette thèse étudie la vérification automatique de propriétés de sûreté de systèmes logico-numériques discrets ou hybrides. Ce sont des systèmes ayant des variables booléennes et numériques et des comportements discrets et continus. Notre approche est fondée sur l'analyse statique par interprétation abstraite. Nous adressons les problèmes suivants : les méthodes d'interprétation abstraite numériques exigent l'énumération des états booléens, et par conséquent, ils souffrent du probléme d'explosion d'espace d'états. En outre, il y a une perte de précision due à l'utilisation d'un opérateur d'élargissement afin de garantir la terminaison de l'analyse. Par ailleurs, nous voulons rendre les méthodes d'interprétation abstraite accessibles à des langages de simulation hybrides. Dans cette thèse, nous généralisons d'abord l'accélération abstraite, une méthode qui améliore la précision des invariants numériques inférés. Ensuite, nous montrons comment étendre l'accélération abstraite et l'itération de max-stratégies à des programmes logico-numériques, ce qui aide à améliorer le compromis entre l'efficacité et la précision. En ce qui concerne les systèmes hybrides, nous traduisons le langage de programmation synchrone et hybride Zelus vers les automates hybrides logico-numériques, et nous étendons les méthodes d'analyse logico-numérique aux systèmes hybrides. Enfin, nous avons mis en oeuvre les méthodes proposées dans un outil nommé ReaVer et nous fournissons des résultats expérimentaux. En conclusion, cette thèse propose une approche unifiée à la vérification de systèmes logico-numériques discrets et hybrides fondée sur l'interprétation abstraite qui est capable d'intégrer des méthodes d'interprétation abstraite numériques sophistiquées tout en améliorant le compromis entre l'efficacité et la précision.

Le sujet de cette thèse est le développement de méthodes pour la découverte automatique des propriétés des variables numériques d'un programme. Nous nous plaçons dans le cadre de l'interprétation abstraite et introduisons plusieurs nouveaux domaines numériques, dont celui des octogones, de coût et de précision intermédiaires entre les domaines non relationnels (peu précis) et relationnels (coûteux) existants. Nous présentons leur adaptation à l'analyse des nombres à virgule flottante, jusqu'à présent limitée aux domaines non relationnels. Enfin, nous présentons les méthodes génériques de linéarisation et de propagation symbolique améliorant leur précision pour un surcoût réduit. Les méthodes introduites dans cette thèse ont été intégr! ées à l'analyseur Astrée et appliquées à la preuve d'absence d'erreurs dans le logiciel embarqué critique de commande de vol des avions Airbus A340, justifiant ainsi l'intérêt de nos méthodes pour des cadres d'applications réelles.

Cette thèse revisite de deux manières le domaine abstrait des polyèdres utilisé pour l'analyse statique de programmes.D'abord, elle montre comment utiliser l'assistant à la preuve Coq pour apporter des garanties sur la correction des opérations sur les polyèdres sans compromettre l'efficacité de l'outil VP Lissu de ces travaux.L'outil est fondé sur le principe de la vérification de résultats :un oracle, auquel on ne fait pas confiance, fait les calculs,puis les résultats sont vérifiés par un validateur dont la correction est prouvée avec Coq. De plus, l'oracle fournit des témoins de la correction des résultats afin d'accélérer la vérification.L'autre caractéristique de VPL est l' utilsation de la seule représentation par contraintes des polyèdres,par opposition à l'approche habituelle qui consiste à utiliser à la fois des contraintes et des générateurs.Malgré ce choix inhabituel,les performances de VPL s'avèrent compétitives.Comme on pouvait le prévoir,l'opérateur "join",qui calcule l'enveloppe convexe de deux polyèdres,est le plus coûteux.Puisqu'il nécessite un grand nombre de projections,cette thèse explore plusieurs nouvelles approches de l'opérateur de projection,basées sur la programmation linéaire paramétrique.Elle propose une synthèse des variantes et des combinaisons possibles.La thèse se termine sur les éléments clés d'un nouvel algorithme de résolution tirant parti des spécificités de l'encodage afin d'obtenir de bonnes performances. / The work reported in this thesis revisits in two waysthe abstract domain of polyhedraused for static analysis of programs.First, strong guarantees are provided on the soundness of the operationson polyhedra,by using of the Coq proof assistant to check the soundness proofs.The means used to ensure correctnessdon't hinder the performance of the resultingVerimag Polyhedra Library (VPL).It is built on the principle of result verification:computations are performed by an untrusted oracleand their results are verified by a checkerwhose correctness is proved in Coq.In order to make verification cheap,the oracle computes soundness witnesses along with the results.The other distinguishing feature of VPL is thatit relies only on the constraint representation of polyhedra,as opposed to the common practice of using both constraints and generators.Despite this unusual choice,VPL turns out to be a competitive abstract domain of polyhedra,performance-wise.As expected, the join operator of VPL,which performs the convex hull of two polyhedra,is the costliest operator.Since it builds on the projection operator,this thesis also investigates a new approach toperforming projections,based on parametric linear programming.A new understanding of projection encoded asa parametric linear problem is presented.The thesis closes on a progress report in the design of a new solvingalgorithm,tailored to the specifics of the encodingso as to achieve good performance.

Les contraintes arithmétiques sont largement utilisées dans les langages formels comme les expressions, les grammaires d'arbres et les chemins réguliers. Ces contraintes sont utilisées dans les modéles de contenu des types (XML Schemas) pour imposer des bornes sur le nombre d'occurrences de nœuds. Dans les langages de requêtes (XPath, XQuery), ces contraintes permettent de sélectionner les nœuds ayant un nombre limité de nœuds accessibles par une expression de chemin donnée. Les types et chemins étendus avec les contraintes de comptage constituent le prolongement naturel de leurs homologues sans comptage déjà considérés comme des constructions fondamentales dans les langages de programmation et les systèmes de type pour XML. Un des défis majeurs en programmation XML consiste à développer des techniques automatisées permettant d'assurer statiquement un typage correct et des optimisations de programmes manipulant les données XML. À cette fin, il est nécessaire de résoudre certaines tâches de raisonnement qui impliquent des constructions telles que les types et les expressions XPath avec des contraintes de comptage. Dans un futur proche, les compilateurs de programmes XML devront résoudre des problèmes de base tels que le sous-typage afin de s'assurer au moment de la compilation qu'un programme ne pourra jamais générer de documents non valides à l'exécution. Cette thèse étudie les logiques capables d'exprimer des contraintes de comptage sur les structures d'arbres. Il a été montré récemment que le mu-calcul sur les graphes, lorsqu'il est étendu à des contraintes de comptage portant exclusivement sur les nœuds successeurs immédiats est indécidable. Dans cette thèse, nous montrons que, sur les arbres finis, la logique avec contraintes de comptage est décidable en temps exponentiel. En outre, cette logique fournit des opérateurs de comptage selon des chemins plus généraux. En effet, la logique peut exprimer des contraintes numériques sur le nombre de nœuds descendants ou même ascendants. Nous présentons également des traductions linéaires d'expressions XPath et de types XML comportant des contraintes de comptage dans la logique. / Arithmetical constraints are widely used in formal languages like regular expressions, tree grammars and paths. In XML they are used to impose bounds on the number of occurrences described by content models of schema languages (XML Schema, RelaxNG). In query languages (XPath, XQuery), they allow selecting nodes that have a bounded number of nodes reachable by a given path expression. Counting types and paths are thus natural extensions of their countless counterparts already regarded as the core constructs in XML languages and type systems. One of the biggest challenges in XML is to develop automated techniques for ensuring static-type safety and optimization techniques. To this end, there is a need to solve some basic reasoning tasks that involve constructions such as counting XML schemas and XPath expressions. Every compiler of XML programs will have to routinely solve problems such as type and path type- checking, for ensuring at compile time that invalid documents can never arise as the output of XML processing code. This thesis studies efficient reasoning frameworks able to express counting constraints on tree structures. It was recently shown that the mu-calculus, when extended with counting constraints on immediate successor nodes is undecid able over graphs. Here we show that, when interpreted over finite trees, the logic with counting constraints is decidable in single exponential time. Furthermore, this logic allows more general counting operators. For example, the logic can pose numerical constraints on number of ancestors or descendants. We also present linear translations of counting XPath expressions and XML schemas into the logic.

Cette thèse présente la nouvelle implémentation de la Verified Polyhedra Library (VPL), une bibliothèque efficace de calcul polyédral.Elle fournit des opérateurs certifiés en Coq, s'appliquant sur des représentations en contraintes.La version précédente souffrait d'inefficacité lors d'opérateurs cruciaux, à savoir l'élimination de variables et l'enveloppe convexe.Dans ce document, je présente des améliorations importantes qui bénéficient à la modularité, la simplicité et au passage à l'échelle de la bibliothèque:le processus de certification est généralisé et simplifié;les conditions polynomiales sont maintenant traitées;Les calculs qui n'impliquent pas de certification sont effectués en flottant;de nouveaux algorithmes sont fournis pour la minimisation de représentation et la détection d'égalités implicites.D'un côté, l'implémentation d'un solveur de problèmes de Programmation Linéaire Paramétrique (PLP) a mené à une meilleure efficacité tant en nombre de contraintes que de générateurs.L'élimination de variables et l'enveloppe convexe sont tous deux encodés en problème PLP.Le PLP est un outil générique possédant de nombreuses applications, et qui permet d'éviter la génération de redondances grâce à l'utilisation d'une contrainte de normalisation.De plus, nous proposons de nouveaux opérateurs pour la gestion des contraintes polynomiales, l'un d'entre eux étant également encodé en tant que problème PLP.De l'autre, la certification de la bibliothèque a été grandement optimisée et simplifiée.La VPL suit un paradigme de vérification a posteriori, où les calculs non triviaux sont effectués par des oracles externes générant des témoins de correction.Ces témoins sont ensuite validés par un vérifieur écrit en Coq.Grâce à un cadre de certification puissant et innovant, le Polymorphic Factory Style (PFS), la plupart des aspects délicats de la génération de témoins sont maintenant évitée.La souplesse du PFS est démontrée par la création d'une tactique en COQ qui découvre les égalités implicites en arithmétique linéaire. / This thesis presents the design and implementation of the Verified Polyhedra Library (VPL), a scalable library for polyhedral calculus.It provides Coq-certified polyhedral operators that work on constraints-only representation.The previous version was inefficient on crucial operations, namely variable elimination and convex hull.In this work, I present major improvements that have been made in scalability, modularity and simplicity:The certification process is generalized and simplified;Polynomial guards can now be handled;Computations that do not involve certification use floating-points;New algorithms are presented for minimization and detection of implicit equalities.On the one hand, the implementation of a solver for Parametric Linear Programming (PLP) problems led to an improved scalability both in dimension and in number of constraints.Variable elimination and convex hull are now encoded as such.PLP is a generic tool that has many applications, and that avoids generating redundancies thanks to a normalization constraint.Additionally, we provide new operators for handling multivariate polynomials, one of which being also encoded as a PLP problem.On the other hand, the certification part of the library has been greatly optimized and simplified.The VPL follows a result-verification paradigm, where complex computations are performed by untrusted oracles that generate witnesses of correctness, themselves validated by a certified Coq checker.Thanks to an innovative and powerful certification framework known as Polymorphic Factory Style (PFS), most cumbersome parts of the witness generation are now avoided.The flexibility of PFS is attested by the creation of a Coq tactic for learning equalities in linear arithmetic.