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.

L'objectif de ce travail de thèse est d'étudier le comportement de l'endommagement des matériaux composites sous chargement statique et fatigue par contrôle non destructif (C.N.D) thermographie et soutenu par émission acoustique et la tomographie (CT scan). Pour cela, ce unidirectionnels composite à fibres de verre (GFRP) et discontinue composite à fibres de carbone (DCFC) ont été utilisés comme les éprouvettes qui ont fourni par PSA peugeot citröen, France. Une série d'essais mécaniques a été réalisée pour déterminer le comportement de l'endommagement sous chargement statique et fatigue. Pendant tout des essais mécanique, la thermographie a été utilisé pour l'observation en temps réel pour suivre l'évolution des températures sur la surface de l'éprouvette et supporté par émission acoustique dans certaines conditions. Cette étude a utilisé une forme rectangulaire et se compose d'éprouvettes trouées et non trouées au centre de l'éprouvette. La vitesse de déplacement constante est appliquée pour observer l'effet sur le comportement de l'endommagement sous chargement de traction statique. Sous les essais de fatigue, le paramètre constant de la fréquence et de l'amplitude de stress a été étudiée pour chaque niveau de charge pour avoir les propriétés de fatigue et l'évolution de l'endommagement de l'éprouvette. La tomographie a été utilisée pour confirmer l'apparition de l'endommagement et l'etat du matériau après l'essai de fatigue. L'analyse des résultats de l'expérimentation et de l'observation NDT montré le bon accord entre les résultats mechnical et NDT thermographie avec prise en charge par l'observation de l'émission acoustique en détecter l'apparition et la propagation de l'endommagement de GFRP PRV et DCFC sous chargement de statique en traction. Les essais en fatigue montrent que la dissipation thermique est liée à l'évolution de l'endommagement et également thermographie et peut être utilisé avec succès pour déterminer la limite d'endurance (HCFS) et la courbe de Wöhler du matériau composite. Les résultats par CT scan ont mesurée avec succès les endommagements et l'état du matériau après essai de fatigue du matériau composite. / The aim of this study is to investigate the damage behaviour of composite material in static and fatigue condition with non destructive testing (NDT) thermography method and supported by acoustic emission and also computed tomography (CT) scan. Thermography and acoustic emission are used in real-time monitoring techniques during the test. On the other hand, NDT observation of tomography is used for a post-failure analysis. In order to achive this, continuous glass fiber composite (GFRP) and discontinuous carbon fiber composite (DCFC) have been used as the test specimens which supplied by PSA Company, France. A series of mechanical testing was carried out to determine the damage behaviour under static and fatigue loading. During all the mechanical testing, thermography was used in real-time observation to follow the temperature change on specimen surface and supported by acoustic emission in certain condition. This study used rectangular shape and consist of specimen with and without circular notches (hole) at the center. The constant displacement rate is applied to observe the effect on damage behaviour under tensile static loading. Under fatigue testing, the constant parameter of frequency and amplitude of stress was explored for each load level to have the fatigue properties and damage evolution of specimen. The tomography was used to confirm the appearance of damage and material condition after fatigue testing. The analysis from the experiment results and NDT observation shown the good agreement between mechnical results and NDT thermography with supported by acoustic emission observation in detect the appearance and propagation of damage for GFRP and DCFC under static loading. Fatigue testing shows that thermal dissipation is related to the damage evolution and also thermography and can be successfully used to determine high cycle fatigue strength (HCFS) and S-N curve of fiber composite material. From post failure analysis, CT scan analysis successfully measured and evaluated damage and material condition after fatigue test for fiber composite material. v

Les produits issus des technologies Silicium tendent à exploiter au maximum les performancesdes transistors MOS tout en les soumettant à des profils de mission très agressifs du point de vuede la fiabilité. Les concepteurs sont ainsi à la recherche du meilleur compromis entre performanceet fiabilité.Historiquement, l’étude de la fiabilité du transistor MOS et le développement des modèlessous jacents ont été menés sur la base de contrainte de vieillissement statique. Avec le développementdes produits à hautes performances dans le domaine de la radiofréquence (RF), laquestion de la fiabilité pour ce type d’application se pose. Ainsi, une extension des modèles defiabilité doit être réalisée afin de quantifier le vieillissement des paramètres clés RF soumis àdes contraintes statiques mais également RF. C’est cette extension de la fiabilité des transistorsMOS dans le domaine RF qui constitue le sujet de ce travail de thèse.Dans ce manuscrit, le fonctionnement du transistor MOS est décrit et sa fiabilité est introduite.Les différents mécanismes de dégradation sont étudiés et leurs modèles associés décrits.Sont ensuite présentés un banc de mesure et une méthodologie nécessaire à l’étude du vieillissementdes transistors dans le domaine RF, ainsi qu’à l’extension des modèles de fiabilité audomaine RF. / Products using nowadays silicon technology are generally targeting aggressive specificationsand push the developers to determine the best compromise between performance and reliability.Main front-end degradation mechanisms are historically studied and modeled under static stressconditions and focus on the static MOS transistor parameters.With the development of product targeting high performances in the radio frequency (RF)domain, the reliability is becoming a first order concern. Thus an extension of the actual staticreliability models must be done to quantify the aging of key RF parameters under static andRF stress. In this context, this work focuses on the extension of the MOS transistor reliabilityregarding the study of RF parameters and also the application of RF stress.After describing the MOS transistor properties, the reliability aspect is introduced and theemphasis is put on the different degradation mechanisms and their associated models. Thisallows the development of an experimental setup and the required methodology to investigatethe device aging in the RF domain and to extend actual static models.

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.

La vérification de logiciels est une activité dont l'importance est cruciale pour les logiciels embarqués critiques. Les différentes approches envisageables peuvent être classées en quatre catégories : les méthodes d'analyse statique non formelles, les méthodes d'analyse statique formelles, les méthodes d'analyse dynamique non formelles et les méthodes d'analyse dynamique formelles. L'objectif de cette thèse est de vérifier des propriétés temporelles dans un cadre industriel, par analyse dynamique formelle.La contribution comporte trois parties. Un langage adapté à l'expression des propriétés à vérifier, tirées du contexte industriel d'Airbus, a été dé ni. Il repose notamment sur la logique temporelle linéaire mais également sur un langage d'expressions régulières.La vérification d'une propriété temporelle s'effectue sur une trace d'exécution d'un logiciel, générée à partir d'un cas de test pré-existant. L'analyse statique est utilisée pour générer la trace en fonction des informations nécessaires à la vérification de la propriété temporelle formalisée.Cette approche de vérification propose une solution pragmatique au problème posé par le caractère ni des traces considérées. Des adaptations et des optimisations ont également été mises en œuvre pour améliorer l'efficacité de l'approche et faciliter son utilisation dans un contexte industriel. Deux prototypes ont été implémentés,des expérimentations ont été menées sur différents logiciels d'Airbus. / Software Verification is decisive for embedded software. The different verification approaches can be classified in four categories : non formal static analysis,formal static analysis, non formal dynamic analysis and formal dynamic analysis.The main goal of this thesis is to verify temporal properties on real industrial applications,with the help of formal dynamic analysis.There are three parts for this contribution. A language, which is well adapted to the properties we want to verify in the Airbus context was defined. This language is grounded on linear temporal logic and also on a regular expression language.Verification of a temporal property is done on an execution trace, generated from an existing test case. Generation also depends on required information to verify the formalized property. Static analysis is used to generate the trace depending on the formalized property.The thesis also proposes a pragmatic solution to the end of trace problem. In addition,specific adaptations and optimisations were defined to improve efficiency and user-friendliness and thus allow an industrial use of this approach. Two applications were implemented. Some experiments were led on different Airbus software.

Cette thèse s'intéresse en premier lieu à l'analyse des effetsfonctionnels des erreurs dans laconfiguration de FPGAs à base de SRAM. Ces erreurs peuvent provenir deperturbations naturelles(rayonnements, particules) ou d'attaques volontaires, par exemple avecun laser. La famille Virtex IIde Xilinx est utilisée comme premier cas pratique d'expérimentation,puis une comparaison est réaliséeavec la famille AT40K de chez ATMEL. Ceci a permis de mieux comprendrel'impact réel dedifférentes sources de perturbations, et les motifs d'erreur devantréellement être pris en compte pouraméliorer la robustesse d'un circuit implanté sur ce type detechnologie. Cette étude a nécessité ledéveloppement d'outils de conception spécifiques, permettantd'automatiser les analyses. Uneméthodologie innovante est proposée pour l'évaluation de lasensibilité de la mémoire de configurationaux SEUs : une classification des bits de configuration est établie enfonction des effets produits parleur inversion sur le fonctionnement normal de l'application. Cecipermet de déterminer les zones lesplus critiques, autorisant le développement de stratégies deprotection sélectives et à faible coût. / This thesis deals primarily with the analysis of the functionaleffects of errors in the configuration ofSRAM-based FPGAs. These errors can be due either to naturalperturbations (radiations, particles) orto malicious attacks, for example with a laser. The Xilinx Virtex IIfamily is used as first case study,then a comparison is made with the ATMEL AT40K family. This workallowed us a betterunderstanding of the real impact of perturbations, and of the errorpatterns that need to be taken intoaccount when improving the robustness of a circuit implemented on thistype of technology. Thisstudy required the development of specific design tools to automatethe analyses. An innovativemethodology is proposed for the evaluation of the configuration memorysensitivity to SEUs: aclassification of configuration bits is made with respect to theeffects produced on the application by asingle bit-flip. This enables us to identify the most critical areas,and to propose selective hardeningsolutions, improving the global reliability of the application at low cost.

Malgré d’excellentes propriétés mécaniques dans le plan, les stratifiés présentent un problème propre aux matériaux réalisés par stratification : le délaminage.Ainsi, ce travail de thèse a pour objet d’analyser le comportement en statique, en fatigue et en vibration linéaire et non linéaire des matériaux composite en présence d’endommagement de type délaminage. Dans ce but nous avons, dans un premier temps mis en place un modèle analytique simplifié, permettant de décrire le comportement élastique en flexion du composite multicouche en fonction de la longueur du délaminage.Une étude expérimentale détaillée a été menée pour caractériser le comportement mécanique en statique et en fatigue de ces matériaux. Des essais ont été conduits en flexion 3-points sur des poutres de ces matériaux pour plusieurs longueurs de délaminage. Ensuite, le comportement en vibration de ces matériaux a été étudié dans le cas de la flexion de poutres. Nous nous sommes intéressés à l’identification de l’amortissement et des propriétés élastiques de ces matériaux et à leur évolution en fonction de la longueur du délaminage.L’étude expérimentale de la réponse en fréquence à une excitation forcée a permis de mesurer les fréquences propres et les amortissements de ces matériaux autour de chaque pic de résonance pour plusieurs longueurs de délaminage. Les résultats déduits de l’analyse expérimentale ont été comparés aux résultats obtenus à partir d’une analyse par éléments finis. Enfin, une méthode de vibration non linéaire a été appliquée pour caractériser le comportement des matériaux composites en présence de délaminage. Les paramètres non linéaires relatifs au décalage fréquentiel et à l’amortissement sont mesurés en faisant varier l’amplitude d’excitation. Cette étude a permis de montrer que les paramètres non linéaires sont plus sensibles au délaminage que les paramètres linéaires. / The aim of this work is to investigate the effects of delamination lengths on the static, fatigue, linear and nonlinear vibration behaviour of composite materials. An analytical model is first presented using laminated beams theory of bending behavior. A study was conducted in static and cyclic fatigue loading with various debonding lengths. Flexural modulus in static tests was determined using the composite plate theory. The effects of delamination lengths on the stiffness, hysteresis loops and damping were studied for various numbers of cycles during fatigue tests. Then, modeling of the damping of a composite with delaminaton was established considering finite element analysis which evaluated the different energies dissipated in the material directions. The effects of delamination variable lengths on natural frequencies and damping were studied numerically and compared with experimental results. Finally, the nonlinear vibration method was used to characterize the behaviour of composite beams with delamination. The nonlinear parameters corresponding to the elastic modulus and damping were determined for each frequency mode and each debonding length. The results showed that nonlinear parameters were much more sensitive to damage than linear parameters.

Nous cherchons à améliorer l'état de l'art des implémentations de contrôle de flux d'information dans les systèmes Linux. Le contrôle de flux d'information vise à surveiller la façon dont l'information se dissémine dans le système une fois hors de son conteneur d'origine, contrairement au contrôle d'accès qui ne peut permettre d'appliquer des règles que sur la manière dont les conteneurs sont accédés. Plusieurs défis scientifiques et techniques se sont présentés. Premièrement, la base de code Linux est particulièrement grande, avec quinze millions de lignes de code réparties dans trente-mille fichiers. La première contribution de cette thèse a été un plugin pour le compilateur GCC permettant d'extraire et visualiser aisément les graphes de flot de contrôle des fonctions du noyau. Ensuite, le framework des Linux Security Modules qui est utilisé pour implémenter les moniteurs de flux d'information que nous avons étudiés (Laminar [1], KBlare [2] et Weir [3]) a été conçu en premier lieu pour le contrôle d'accès, et non de flux. La question se pose donc de savoir si le framework est implémenté de telle sorte à permettre la capture de tous les flux produits par les appels système. Nous avons créé et implémenté une analyse statique permettant de répondre à ce problème. Cette analyse statique est implémenté en tant que plugin GCC et nous a permis d'améliorer le framework LSM pour capturer tous les flux. Enfin, nous avons constaté que les moniteurs de flux actuels n'étaient pas résistants aux conditions de concurrence entre les flux et ne pouvaient pas traiter certains canaux ouverts tels que les projections de fichiers en mémoire et les segments de mémoire partagée entre processus. Nous avons implémenté Rfblare, un nouvel algorithme de suivi de flux, pour KBlare, dont nous avons prouvé la correction avec Coq. Nous avons ainsi montré que LSM pouvait être utilisé avec succès pour implémenter le contrôle de flux d'information, et que seules les méthodes formelles, permettant la mise en œuvre de méthodologie, d'analyses ou d'outils réutilisables, permettaient de s'attaquer à la complexité et aux rapides évolutions du noyau Linux. / We look forward to improving the implementations of information flow control mechanisms in Linux Operating Systems. Information Flow Control aims at monitoring how information disseminates in a system once it is out of its original container, unlike access control which can merely apply rule on how the containers are accessed. We met several scientific and technical challenges. First of all, the Linux codebase is big, over fifteen millions lines of code spread over thirty three thousand files. The first contribution of this thesis is a plugin for the GCC compiler able to extract and let a user easily visualize the control flow graphs of the Linux kernel functions. Secondly, the Linux Security Modules framework which is used to implement the information flow trackers we have reviewed (Laminar, KBlare, and Weir) was designed in the first place to implement access control, rather than information flow control. One issue is thus left open: is the framework implemented in such a way that all flows generated by system calls can be captured? We have created and implemented static analysis to address this problem and proved its correction with the Coq proof assistant system. This analysis is implemented as a GCC plugin and have allowed us to improve the LSM framework in order to capture all flows. Finally, we have noted that current information flow trackers are vulnerable to race conditions between flows and are unable to cover some overt channels of information such as files mapping to memory and shared memory segments between processes. We have implemented Rfblare, a new algorithm of flow tracking, for KBlare. The correction of this algorithm has been proved with Coq. We have showed that LSM can be used successfully to implement information flow control, and that only formal methods, leading to reusable methodology, analysis, tools, etc., are a match for the complexity and the fast-paced evolution of the Linux kernel.