Les circuits microélectroniques récents intègrent des dizaines d'horloges afin d'optimiser leur consommation et leur performance. Le nombre de traversées de domaines d'horloges (CDC) et la complexité des systèmes augmentant, garantir formellement l'intégrité d'une donnée devient un défi majeur. Plusieurs problèmes sont alors soulevés : configurer le système dans un mode réaliste, décrire l'environnement par des hypothèses sur les protocoles, gérer l'explosion de l'espace des états, analyser les contre-exemples, ...La première contribution de cette thèse a pour but d'atteindre une configuration complète et réaliste du système. Nous utilisons de la vérification formelle paramétrique ainsi qu'une analyse de la structure du circuit afin de détecter automatiquement les composants des arbres d'horloge. La seconde contribution cherche à éviter l'explosion de l'espace des états en combinant des abstractions localisées du circuit avec une analyse de contre-examples. L'idée clé est d'utiliser la technologie de raffinement d'abstraction guidée par contre-exemple (CEGAR) où l'utilisateur influence la poursuite de l'algorithme en se basant sur des informations extraites des contre-exemples intermédiaires. La troisième contribution vise à créer des hypothèses pour des environnements sous-contraints. Tout d’abord, plusieurs contre-exemples sont générés pour une assertion, avec différentes raisons d’échec. Ensuite, des informations en sont extraites et transformées en hypothèses réalistes.Au final, cette thèse montre qu'une vérification formelle concluante peut être obtenue en combinant la rapidité de l'analyse structurelle avec l'exhaustivité des méthodes formelles. / Modern hardware designs typically comprise tens of clocks to optimize consumption and performance to the ongoing tasks. With the increasing number of clock-domain crossings as well as the huge complexity of modern SoCs, formally proving the functional integrity of data propagation became a major challenge. Several issues arise: setting up the design in a realistic mode, writing protocol assumptions modeling the environment, facing state-space explosion, analyzing counter-examples, ...The first contribution of this thesis aims at reaching a complete and realistic design setup. We use parametric liveness verification and a structural analysis of the design in order to identify behaviors of the clock and reset trees. The second contribution aims at avoiding state-space explosion, by combining localization abstractions of the design, and counter-example analysis. The key idea is to use counterexample-guided abstraction refinement as the algorithmic back-end, where the user influence the course of the algorithm based on relevant information extracted from intermediate abstract counterexamples. The third contribution aims at creating protocol assumptions for under-specified environments. First, multiple counter-examples are generated for an assertion, with different causes of failure. Then, information is mined from them and transformed into realistic protocol assumptions.Overall, this thesis shows that a conclusive formal verification can be obtained by combining inexpensive structural analysis along with exhaustive model checking.

Garantir la sécurité d’une application tout au long de son cycle de vie est une tâche fastidieuse. Le choix, l’implémentation et l’évaluation des solutions de sécurité est difficile et sujette a des erreurs. Les compétences en sécurité ne sont pas répondues dans toutes les équipes de développement. Afin de réduire ce manque de compétences en sécurité, les développeurs ont a leurs disposition une multitude de documents décrivant des problèmes de sécurité et des solutions requises (i.e., vulnérabilités, attaques, principes de sécurité, patrons sécurité, etc.). Abstraites et informelles, ces documents sont fournis par des sources différentes et leur nombre est en constante croissance. Les développeurs sont noyés dans une multitude de documents ce qui fait obstruction à leur capacité à choisir, implémenter et évaluer la sécurité d’une application. Cette thèse aborde ces questions et propose un ensemble de méthodes pour aider les développeurs à choisir, implémenter et évaluer les solutions de sécurité face aux problèmes de sécurité. Ces problèmes sont matérialisés par les failles, les vulnérabilités, les attaques, etc. et les solutions fournies par des patrons de sécurité. Cette thèse introduit en premier une méthode pour aider les développeurs dans l’implémentation de patrons de sécurité et l’estimation de leur efficacité face aux vulnérabilités. Puis elle présente trois méthodes associant les patrons de sécurité, les vulnérabilités, les attaques, etc. au sein d’une base de connaissance. Cette dernière permet une extraction automatique de classifications de patrons et améliore la rapidité et la précision des développeurs dans le choix des patrons de sécurité face à une vulnérabilité ou une attaque. En utilisant la base de connaissance, nous présentons une méthode pour aider les développeurs dans la modélisation des menaces ainsi que la générations et l’exécution des cas de test de sécurité. La méthode est évaluée et les résultats montrent que la méthode améliore l’efficacité, la compréhensibilité et la précision des développeurs dans le choix des patrons de sécurité et d’écriture des cas de test de sécurité. / Ensuring the security of an application through its life cycle is a tedious task. The choice, the implementation and the evaluation of security solutions is difficult and error prone. Security skills are not common in development teams. To overcome the lack of security skills, developers and designers are provided with a plethora of documents about security problems and solutions (i.e, vulnerabilities, attacks, security principles, security patterns, etc.). Abstract and informal, these documents are provided by different sources, and their number is constantly growing. Developers are drown in a sea of documentation, which inhibits their capacity to design, implement, and the evaluate the overall application security. This thesis tackles these issues and presents a set of approaches to help designers in the choice, the implementation and the evaluation of security solutions required to overcome security problems. The problems are materialized by weaknesses, vulnerabilities, attacks, etc. and security solutions are given by security patterns.This thesis first introduces a method to guide designers implement security patterns and assess their effectiveness against vulnerabilities. Then, we present three methods associating security patterns, attacks, weaknesses, etc. in a knowledge base. This allows automated extraction of classifications and help designers quickly and accurately select security patterns required to cure a weakness or to overcome an attack. Based on this nowledge base, we detaila method to help designers in threat modeling and security test generation and execution. The method is evaluated and results show that the method enhances the comprehensibility and the accuracy of developers in the security solutions choice, threat modeling and in the writing of security test cases.

La programmation par contraintes offre des langages et des outils permettant de résoudre des problèmes à forte combinatoire et à la complexité élevée tels que ceux qui existent en vérification de programmes. Dans cette thèse nous résolvons deux familles de problèmes de la vérification de programmes. Dans chaque cas de figure nous commençons par une étude formelle du problème avant de proposer des modèles en contraintes puis de réaliser des expérimentations. La première contribution concerne un langage réactif synchrone représentable par une algèbre de diagramme de blocs. Les programmes utilisent des flux infinis et modélisent des systèmes temps réel. Nous proposons un modèle en contraintes muni d’une nouvelle contrainte globale ainsi que ses algorithmes de filtrage inspirés de l’interprétation abstraite. Cette contrainte permet de calculer des sur-approximations des valeurs des flux des diagrammes de blocs. Nous évaluons notre processus de vérification sur le langage FAUST, qui est un langage dédié à la génération de flux audio. La seconde contribution concerne les systèmes probabilistes représentés par des chaînes de Markov à intervalles paramétrés, un formalisme de spécification qui étend les chaînes de Markov. Nous proposons des modèles en contraintes pour vérifier des propriétés qualitatives et quantitatives. Nos modèles dans le cas qualitatif améliorent l’état de l’art tandis que ceux dans le cas quantitatif sont les premiers proposés à ce jour. Nous avons implémenté nos modèles en contraintes en problèmes de programmation linéaire en nombres entiers et en problèmes de satisfaction modulo des théories. Les expériences sont réalisées à partir d’un jeu d’essais de la bibliothèque PRISM. / Constraint programming offers efficient languages andtools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming.In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments.The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.

La réutilisation est une pratique courante lors du développement de logiciel. Bien souvent, cette réutilisation se fait à travers l’utilisation des librairies. Cette dernière met ses fonctionnalités à disposition des développeurs en utilisant les Interfaces de Programmation d’Application (API). En théorie, les développeurs qui utilisent les API n’ont pas forcément besoin de se préoccuper de comment les éléments internes de cette API fonctionnent. En effet, les API mettent leurs fonctionnalités à disposition des développeurs sans forcément dévoiler ce qui se passe à l’interne. Cependant, pour utiliser correctement une API il est nécessaire de respecter des contraintes d’utilisation qui sont à la fois implicites et explicites ainsi que des modèles d’utilisation. L’usage des librairies et des API est très commun dans le domaine du développement de logiciel. Cela permet aux développeurs d’utiliser les fonctionnalités proposées par l’API et ainsi de se concentrer directement sur la tâche qu’ils doivent effectuer. Toutefois, apprendre et se familiariser avec les contraintes d’usage des API sont des tâches ardues et exigent un effort cognitif considérable de la part du développeur. Les chercheurs ont tenté de corriger ce problème en étudiant les modèles d’utilisation et en analysant les traces d’utilisation de code client pour s’assurer de leurs conformités. Néanmoins, les analyses dynamiques ne sont pas possibles pendant les phases précoces de développement du logiciel, car cela requiert une implémentation minimum et l’exécution du code. Nous proposons l’outil Temporal Usage PAttern Checker (Tupac). Une approche basée sur l’analyse statique interprocédural pour vérifier la conformité du code client aux modèles d’utilisation pendant la phase de développement. Tupac peut être déployé dans un envi- ronnement de développement (IDE) et ainsi fournir des informations relatives à l’utilisation des API plus tôt pendant la phase de développement du logiciel. Nous avons évalué notre approche sur quatre projets Java avec quatre API. Les résultats ont démontré que Tupac a une bonne précision et un taux de rappel intéressant. De plus, nous avons pu conclure qu’en moyenne cela prend une demi-seconde pour vérifier la confor- mité d’un patron pour un projet tout entier. Cela démontre que Tupac peut être déployé dans un rythme de codage régulier. / In modern software development, reuse takes the form of using libraries that expose their functionality via Application Programming Interfaces (APIs). In theory, APIs allow developers to write client code that reuses library code without needing to know its internals. In practice, correctly using APIs requires respecting explicit and implicit constraints and usage patterns. This allows developers to use functionality proposed by API so that they can focus directly on the task they want to achieve. APIs require a significant effort from the developer to learn various usage constraint. Ignoring such patterns could lead to errors and design flaws. These often cannot be detected prior to integration and system testing. Researchers have attempted to solve this problem by extracting API usage patterns and analyzing client code traces for conformance. However, dynamic analysis is still impossible to perform early without a minimum of integration and execution. We propose the Temporal Usage PAttern Checker (Tupac) for API, an interprocedural static analysis approach that can verify that client code conforms to temporal API usage patterns as it is being developed. Tupac can be deployed inside an Integrated Development Environment (IDE), thus providing developers with feedback about API usage much earlier in the development process. We evaluated the effectiveness of our approach on four projects with four different APIs. Our evaluation shows that Tupac has good precision and interesting recall. Crucially, we also show that it takes, on average, half a second to check an entire project for conformance to a pattern, meaning that it can realistically be deployed in the regular coding rhythm

Avec l'évolution des technologies, la complexité des systèmes informatiques ne cesse de s'accroître. Parmi ces systèmes, on retrouve les logiciels critiques qui doivent offrir une garantie de sûreté de fonctionnement qui s'avère crucial et pour lesquels un dysfonctionnement peut avoir des conséquences graves. Les méthodes formelles fournissent des outils permettant de garantir mathématiquement l'absence de certaines erreurs. Ces méthodes sont indispensables pour assurer les plus hauts niveaux de sûreté. Mais l'application de ces méthodes sur un code système bas niveau se heurte à des difficultés d'ordre pratique et théorique. Les principales difficultés concernent la prise en compte des aspects bas niveau, comme les pointeurs et les interactions avec le matériel spécifique. De plus, le fait que ces systèmes soient concurrents conduit à une augmentation exponentielle du nombre de comportements possibles, ce qui rend plus difficile leur vérification. Dans cette thèse, nous proposons une méthodologie pour la spécification et la vérification par model-checking de ce type de systèmes, en particulier, ceux implémentés en C. Cette méthodologie est basée sur la traduction de la sémantique de C en TLA+, un langage de spécification formel adapté à la modélisation de systèmes concurrents. Nous avons proposé un modèle de mémoire et d'exécution d'un programme C séquentiel en TLA+. En se basant sur ce modèle, nous avons proposé un ensemble de règles de traduction d'un code C en TLA+ que nous avons implémenté dans un outil, appelé C2TLA+. Nous avons montré comment ce modèle peut s'étendre pour modéliser les programmes C concurrents et gérer la synchronisation entre plusieurs processus ainsi que leur ordonnancement. Pour réduire la complexité du model-checking, nous avons proposé une technique permettant de réduire significativement la complexité de la vérification. Cette réduction consiste pour un code C à agglomérer une suite d'instructions lors de la génération du code TLA+, sous réserve d'un ensemble de conditions.Nous avons appliqué la méthodologie proposée dans cette thèse sur un cas d'étude réel issu de l'implémentation d'un micronoyau industriel,sur lequel nous avons vérifié un ensemble de propriétés fonctionnelles. L'application de la réduction a permis de réduire considérablement le temps de la vérification, ce qui la rend utilisable en pratique.Les résultats ont permis d'étudier le comportement du système, de vérifier certaines propriétés et de trouver des bugs indétectables par des simples tests. / Software systems are critical and complex. In order to guarantee their correctness, the use of formal methodsis important. These methods can be defined as mathematically based techniques, languages and tools for specifying and reasoning about systems. But, the application of formal methods to software systems, implemented in C, is challenging due to the presence of pointers, pointer arithmetic andinteraction with hardware. Moreover, software systems are often concurrent, making the verification process infeasible. This work provides a methodology to specify and verify C software systems usingmodel-checking technique. The proposed methodology is based on translating the semantics of Cinto TLA+, a formal specification language for reasoning about concurrent and reactive systems. We define a memory and execution model for a sequential program and a set of translation rules from C to TLA+ that we developed in a tool called C2TLA+. Based on this model, we show that it can be extended to support concurrency, synchronization primitives and process scheduling. Although model-checking is an efficient and automatic technique, it faces the state explosion problem when the system becomes large. To overcome this problem, we propose a state-space reduction technique. The latter is based on agglomerating a set of C instructions during the generation phase of the TLA+ specification. This methodology has been applied to a concrete case study, a microkernel of an industrial real-time operating system, on which a set of functional properties has been verified. The application of the agglomeration technique to the case study shows the usefulness of the proposed technique in reducing the complexity of verification. The obtained results allow us to study the behavior of the system and to find errors undetectable using traditional testing techniques.

Le sujet de la thèse porte sur la mise en place d’approches numériques avancées pour la simulation et l’optimisation de structures mécaniques présentant une géométrie complexe. Il se focalise sur l’analyse isogéométrique (IGA) qui a reçu beaucoup d’intérêt cette dernière décennie dû à sa grande flexibilité, précision, et robustesse dans de nombreux contextes industriels comparé à la méthode des éléments finis (FEA) classique. En particulier, la technologie IGA fournit un lien direct avec les logiciels de CAO (les mêmes fonctions sont utilisées pour la représentation de la géométrie et l’analyse numérique) et facilite les procédures de maillage.Dans ce contexte, et comme première partie du travail, une méthode de vérification basée sur la dualité et le concept d’erreur en relation de comportement (ERC) est proposé. Il permet d’obtenir des estimateurs d’erreur a posteriori à la fois garantis et entièrement calculables pour les solutions numériques issues de simulation par IGA. Ces estimateurs, valables pour une large gamme de modèles linéaires ou non-linéaires en mécanique des structures, constituent donc des outils performants et utiles pour le contrôle quantitatif de la qualité numérique et pour la conduite de procédures adaptatives. Un intérêt particulier est porté sur la construction de champs équilibrés, qui est un point clé du concept ERC, et qui jusqu’à présent était essentiellement développée dans le cadre de la méthode des éléments finis. L’extension au contexte IGA nécessite d’aborder plusieurs problèmes techniques, liés à l’utilisation de fonctions de base B-Spline/NURBS. Le concept ERC est aussi mis en oeuvre avec les techniques d’adjoint pour faire de l’estimation d’erreur sur des quantités d’intérêt.Dans une seconde partie du travail, la technologie IGA est couplée avec une procédure de réduction de modèle pour obtenir des solutions certifiées, et en temps réel, de problèmes avec une géométrie paramétrée. Après avoir défini le paramétrage sur la transformation permettant de passer de l’espace paramétrique IGA à l’espace physique, un modèle réduit basé sur la technique PGD (Proper Generalized Decomposition) est introduit pour résoudre le problème multi-dimensionnel. Avec une stratégie hors-ligne/en-ligne, la procédure permet alors de décrire l’ensemble des solutions paramétrées avec un coût de calcul réduit, et de faire de l’optimisation de forme en temps réel. Ici encore, l’estimation a posteriori des diverses sources d’erreur venant de la discrétisation et de la réduction de modèle PGD est menée à partir du concept ERC. Cela permet de contrôler la qualité de la solution PGD approchée (globalement ou sur des quantités d’intérêt), pour toute configuration géométrique, et de nourrir un algorithme adaptatif qui optimise l’effort de calcul pour une tolérance d’erreur donnée.Le travail de recherche dans son ensemble fournit donc des outils pertinents et pratiques pour les activités de simulation en ingénierie mécanique. Le potentiel et les performances de ces outils sont montrés à travers plusieurs exemples numériques impliquant des problèmes académiques et industriels, et des modèles linéaires et non-linéaires (endommagement). / The topic of the PhD thesis deals with the construction of advanced numerical approaches for the simulation and optimization of mechanical structures with complex geometry. It focuses on the Isogeometric Analysis (IGA) technology which has received much attention of the last decade due to its increased flexibility, accuracy, and robustness in many engineering simulations compared to classical Finite Element Analysis (FEA). In particular, IGA enables a direct link with CAD software (the same functions are used for both analysis and geometry) and facilitates meshing procedures.In this framework, and as a first part of the work, a verification method based on duality and the concept of Constitutive Relation Error (CRE) is proposed. It enables to derive guaranteed and fully computable a posteriori error estimates on the numerical solution provided by IGA. Such estimates, which are valid for a wide class of linear or nonlinear structural mechanics models, thus constitute performing and useful tools to quantitatively control the numerical accuracy and drive adaptive procedures. The focus here is on the construction of equilibrated flux fields, which is key ingredient of the CRE concept, and which was until now almost exclusively developed in the FEA framework alone. The extension to IGA requires to address some technical issues, due to the use of B-Spline/NURBS basis functions. The CRE concept is also implemented together with adjoint techniques in order to perform goal-oriented error estimation.In a second part, IGA is coupled with model reduction in order to get certified real-time solutions to problems with parameterized geometry. After defining the parametrization on the mapping from the IGA parametric space to the physical space, a reduced model based on the Proper Generalized Decomposition (PGD) is introduced to solve the multi-dimensional problem. From an offline/online strategy, the procedure then enables to describe the manifold of parametric solutions with reduced CPU cost, and to further perform shape optimization in real-time. Here again, a posteriori estimation of the various error sources inheriting from discretization and PGD model reduction is performed from the CRE concept. It enables to control the quality of the approximate PGD solution (globally or on outputs of interest), for any geometry configuration, and to feed a robust greedy algorithm that optimizes the computational effort for a prescribed error tolerance.The overall research work thus provides for reliable and practical tools in mechanical engineering simulation activities. Capabilities and performance of these tools are shown on several numerical experiments with academic and engineering problems, and with linear and nonlinear (damage) models.