Les logiciels évoluent au fil du temps avec la modification, l’ajout et la suppression de nouvelles classes, méthodes, fonctions, dépendances. Une conséquence est que le comportement peut être placé dans de mauvais paquetages et casser la modularité du logiciel. Une bonne organisation des classes dans des paquetages identifiables facilite la compréhension, la maintenance, les tests et l’évolution des logiciels. Nous soutenons que les responsables manquent d’outils pour assurer la remodularisation logicielle. La maintenance des logiciels nécessite des approches qui aident à (i) la compréhension de la structure au niveau du paquetage et l’évaluation de sa qualité; (ii) l’identification des problèmes de modularité, et (iii) la prise de décisions pour le changement.Dans cette thèse nous proposons ECOO, une approche qui aide la remodularisation. Elle concerne les trois domaines de recherche suivants:- Comprendre les problèmes de dépendance entre paquetages. Nous proposons des visualisations mettant en évidence les dépendances cycliques au niveau des paquetages.- Proposer des dépendances qui devraient être changées. L’approche propose des dépendances à changer pour rendre le système plus modulaire.- Analyser l’impact des changements. L’approche propose une analyse d’impact du changement pour essayer les modifications avant de les appliquer sur le système réel. L’approche présentée dans cette thèse a été validée qualitativement et les résultats ont été pris en compte dans la réingénierie des systèmes analysés. Les résultats obtenus démontrent l’utilité de notre approche. / Software evolves over time with the modification, addition and removal of new classes, methods, functions, dependencies. A consequence is that behavior may not be placed in the right packages and the software modularization is broken. A good organization of classes into identifiable and collaborating packages eases the understanding, maintenance, test and evolution of software systems. We argue that maintainers lack tool support for understanding the concrete organization and for structuring packages within their context. Our claim is that the maintenance of large software modularizations needs approaches that help (i) understanding the structure at package level and assessing its quality; (ii) identifying modularity problems; and (iii) take decisions and verify the impact of these decisions.In this thesis, we propose ECOO, an approach to help reengineers identify and understand structural problems in software architectures and to support the remodularization activity. It concerns the three following research fields:- Understanding package dependency problems. We propose visualizations to highlight cyclic dependencies problems at package level.- Proposing dependencies to be changed for remodularization. The approach proposes dependencies to break to make the system more modular.- Analyzing impact of change. The approach proposes a change impact analysis to try modifications before applying them on the real system.The approaches presented in this thesis have been qualitatively and quantitatively validated and results have been taken into account in the reengineering of analyzed systems. The results we obtained demonstrate the usefulness of our approach.

L'analyse des dépendances de flot de données est une étape cruciale lors de la parallélisation. La description détaillée des dépendances entre opérations et pour chaque élément de tableau rend possible l'application de techniques de parallélisation performantes. Cependant, ce type d'analyse a deux principaux inconvénients~: son coût élevé et son domaine restreint à des dépendances affines en fonction des compteurs de boucles. On décrit d'abord dans cette thèse un algorithme polynômial pour le calcul des dépendances affines, dont la complexité et le domaine d'application sont meilleurs que ceux des méthodes existantes. Puis, dans la continuité des travaux de J.-F. Collard, on propose un cadre général pour l'analyse, éventuellement approchée, de n'importe quelle dépendance. Le modèle de programmes est formé des programmes sans procédure, comportant des accès quelconques aux éléments de tableaux. Une méthode itérative originale trouve des propriétés entre les contraintes non-affines du problème afin d'améliorer la précision du résultat. Notre méthode est capable de tirer parti de n'importe quelle caractérisation affine de ces contraintes et possède un critère d'optimalité de l'approximation. Enfin, plusieurs applications traditionnelles de l'analyse de flot de données sont adaptées à notre méthode approchée et nous détaillons plus particulièrement l'expansion mémoire, en donnant une méthode offrant un compromis entre surcoût à l'exécution, taille mémoire et degré de parallélisme.

L'industrie des semi-conducteurs continue ses progrès impressionnants dans la miniaturisation des circuits intégrés VLSI. Les concepteurs ont inventé des méthodes permettant d'exploiter la complexité croissante des circuits intégrés à haute densité d'intégration. L'une d'elles consiste à concevoir des systèmes embarqués sur puce (SoC) à l'aide de blocs pré-existants et déjà validés (appelés IP, comme Intellectual Property), qu'ils aient été élaborés en interne à l'entreprise réalisant l'intégration du SoC ou issus d'une tierce partie. Disposer d'une bibliothèque de blocs IP paramétrés selon leurs performances en temps, surface et consommation est une clef pour optimiser le système intégré vis-à-vis de l'application ciblée. S'il existe un flot standard bien établi pour concevoir les blocs intégrés numériques, reposant sur une méthode de conception descendante, la conception de circuits analogiques reste toujours une opération sur mesure. Alors que les systèmes intégrés sur puce sont souvent mixtes analogique-numérique, les méthodes de conception diffèrent complètement entre les deux mondes. Dans cette thèse, nous proposons une méthode pour automatiser le dimensionnement et la polarisation d'un circuit analogique dans le cas général, conduisant ainsi à une définition possible d'un IP analogique. Cette méthode permet de générer automatiquement une procédure pour calculer les dimensions d'une topologie électrique connue et son point de fonctionnement en se fondant sur l'expression de la connaissance du concepteur. Cette méthode permet de détecter des hypothèses conflictuelles émises par le concepteur et de traiter les cycles résultant des boucles de contre-réaction. Plusieurs circuits analogiques sont présentés pour illustrer la généralité et la précision de cette approche.

Les logiciels critiques nécessitent l'obtention d'une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild'analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d'information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d'outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d'ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d'information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d'uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d'une définition formellede la notion de dépendance, à l'aide de l'assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l'analyse de toléranceaux pannes.

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes. / Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis.

Dans le domaine de la vérification formelle de logiciels, il est impératif d'identifier les limites au sein desquelles les éléments ou fonctions opèrent. Ces limites constituent les propriétés de frame (frame properties en anglais). Elles sont habituellement spécifiées manuellement par le programmeur et leur validité doit être vérifiée: il est nécessaire de prouver que les opérations du programme n'outrepassent pas les limites ainsi déclarées. Dans le contexte de la vérification formelle interactive de systèmes complexes, comme les systèmes d'exploitation, un effort considérable est investi dans la spécification et la preuve des propriétés de frame. Cependant, la plupart des opérations ont un effet très localisé et ne menacent donc qu'un nombre limité d'invariants. Étant donné que la spécification et la preuve de propriétés de frame est une tache fastidieuse, il est judicieux d'automatiser l'identification des invariants qui ne sont pas affectés par une opération donnée. Nous présentons dans cette thèse une solution inférant automatiquement leur préservation. Notre solution a pour but de réduire le nombre de preuves à la charge du programmeur. Elle est basée sur l'analyse statique, et ne nécessite aucune annotation de frame. Notre stratégie consiste à combiner une analyse de dépendances avec une analyse de corrélations. Nous avons conçu et implémenté ces deux analyses statiques pour un langage fonctionnel fortement typé qui manipule structures, variants et tableaux. Typiquement, une propriété fonctionnelle ne dépend que de quelques fragments de l'état du programme. L'analyse de dépendances détermine quelles parties de cet état influent sur le résultat de la propriété fonctionnelle. De même, une fonction ne modifiera que certaines parties de ses arguments, copiant le reste à l'identique. L'analyse de corrélations détecte quelles parties de l'entrée d'une fonction se retrouvent copiées directement (i.e. non modifiés) dans son résultat. Ces deux analyses calculent une approximation conservatrice. Grâce aux résultats de ces deux analyses statiques, un prouveur de théorèmes interactif peut inférer automatiquement la préservation des invariants qui portent sur la partie non affectée par l’opération concernée. Nous avons appliqué ces deux analyses statiques à la spécification fonctionnelle d'un micro-noyau, et obtenu des résultats non seulement d'une précision adéquate, mais qui montrent par ailleurs que notre approche peut passer à l'échelle. / In the field of software verification, the frame problem refers to establishing the boundaries within which program elements operate. It has notoriously tedious consequences on the specification of frame properties, which indicate the parts of the program state that an operation is allowed to modify, as well as on their verification, i.e. proving that operations modify only what is specified by their frame properties. In the context of interactive formal verification of complex systems, such as operating systems, much effort is spent addressing these consequences and proving the preservation of the systems' invariants. However, most operations have a localized effect on the system and impact only a limited number of invariants at the same time. In this thesis we address the issue of identifying those invariants that are unaffected by an operation and we present a solution for automatically inferring their preservation. Our solution is meant to ease the proof burden for the programmer. It is based on static analysis and does not require any additional frame annotations. Our strategy consists in combining a dependency analysis and a correlation analysis. We have designed and implemented both static analyses for a strongly-typed, functional language that handles structures, variants and arrays. The dependency analysis computes a conservative approximation of the input fragments on which functional properties and operations depend. The correlation analysis computes a safe approximation of the parts of an input state to a function that are copied to the output state. It summarizes not only what is modified but also how it is modified and to what extent. By employing these two static analyses and by subsequently reasoning based on their combined results, an interactive theorem prover can automate the discharching of proof obligations for unmodified parts of the state. We have applied both of our static analyses to a functional specification of a micro-kernel and the obtained results demonstrate both their precision and their scalability.