La thèse s'inscrit dans le domaine de la modélisation et de la validation des systèmes modernes complexes. Les systèmes actuels sont en fait d'une complexité sans cesse croissante et formés de plus en plus de composants de natures différentes. Ceci rend leur processus de conception et de validation coûteux et difficile. Il semble être la simple façon permettant de faire face à cette hétérogénéité et à cette complexité est l'approche orientée composant. Suivant cette approche, le système est une entité formée par un ensemble des composants interconnectés. Les composants définissent une interface qui permet d'abstraire leur modèle interne (boîte noire), ce qui favorise la modularité et la réutilisation des composants. L'interaction entre ces composants se fait conformément à un ensemble des règles pré-établies, permettant ainsi d'avoir une vision globale de comportement du système. La conception ainsi que la validation des systèmes modernes reste alors problématique à cause de la nécessité de prendre en compte l'hétérogénéité des différents composants. Dans ce cadre, dans un premier temps, nous définirons un cadre formel générique dans lequel une large famille de formalismes de description de systèmes à base d'états peut être naturellement capturée. Ainsi, nous allons définir un ensemble de règles de composition permettant de mettre en correspondance les différents composants et ainsi de constituer un modèle global du système à concevoir. Dans un second temps, nous proposerons une approche de test d'intégration qui permet de valider le comportement d'un système complexe sous l'hypothèse que chaque composant est testé et validé. Cette approche vise à générer automatiquement des cas de test en s'appuyant sur un modèle global décrit dans notre framework du système sous test.

Cette thèse porte sur la spécification, la vérification et la validation de systèmes critiques à l'aide de méthodes formelles, en particulier, B événementiel. Nous avons travaillé sur l'utilisation de B événementiel pour étudier des algorithmes de contrôle du platooning, à partir d'une version 1D simplifiée vers une version 2D plus réaliste. L'analyse critique du modèle du platooning en 1D a découvert certaines anomalies. La difficulté d'exprimer les théorèmes de deadlock-freeness dans B événementiel nous a motivé pour développer un outil, le générateur de théorèmes de deadlock-freeness, pour construire automatiquement ces théorèmes. Notre évaluation a confirmé que les preuves mathématiques ne sont pas suffisantes pour vérifier la correction d'une spécification formelle : une spécification formelle doit aussi être validée. Nous pensons que les activités de validation, comme les activités de vérification, doivent être associées à chaque raffinement. Pour ce faire, nous avons besoin de meilleurs outils de validation. Certains outils d'exécution existants échouent pour certains modèles non-déterministes exprimés en B événementiel. Nous avons donc conçu et implanté un nouvel outil d'exécution, JeB, un environnement de simulation en JavaScript pour B événementiel. JeB permet aux utilisateurs d'insérer du code sûr à la main pour fournir des calculs déterministes lorsque la traduction automatique échoue. Pour atteindre cet objectif, nous avons défini des obligations de preuve qui garantissent la correction de simulations par rapport au modèle formel.

Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Cette thèse présente un algorithme qui élimine les racines carrées et les divi- sions dans des programmes sans boucles, utilisés dans des systèmes embarqués, tout en préservant la sémantique. L'élimination de ces opérations permet d'éviter les erreurs d'arrondis à l'exécution, ces erreurs d'arrondis pouvant entraîner un comportement complètement inattendu de la part du programme. Cette trans- formation respecte les contraintes du code embarqué, en particulier la nécessité pour le programme produit de s'exécuter en mémoire fixe. Cette transformation utilise deux algorithmes fondamentaux développés dans cette thèse. Le premier permet d'éliminer les racines carrées et les divisions des expressions booléennes contenant des comparaisons d'expressions arithmétiques. Le second est un algo- rithme qui résout un problème d'anti-unification particulier, que nous appelons anti-unification contrainte. Cette transformation de programme est définie et prou- vée dans l'assistant de preuves PVS. Elle est aussi implantée comme une stratégie de ce système. L'anti-unification contrainte est aussi utilisée pour étendre la transformation à des programmes contenant des fonctions. Elle permet ainsi d'éliminer les racines carrées et les divisions de spécifications écrites en PVS. La robustesse de cette méthode est mise en valeur par un exemple conséquent: l'élimination des racines carrées et des divisions dans un programme de détection des conflits aériens.

Dans cette thèse nous étudions l'isolation mémoire et les mesures de communications efficaces par passage de message dans le contexte des environnements à mémoire partagée et la programmation orientée-objets. L'état de l'art en la matière se base presque exclusivement sur deux techniques complémentaires dites de propriété des objets (ownership) et d'unicité de références (reference uniqueness) afin d'adresser les problèmes de sécurité dans les programmes concurrents. Il est frappant de constater que la grande majorité des travaux existants emploient des méthodes de vérification statique des programmes, qui requirent soit un effort d'annotations soit l'introduction de fortes contraintes sur la forme et les références vers messages échangés. Notre contribution avec SIAAM est la démonstration d'une solution d'isolation réalisée uniquement à l'exécution et basée sur le modèle de programmation par acteurs. Cette solution purement dynamique ne nécessite ni annotations ni vérification statique des programmes. SIAAM permet la communication sans copie de messages de forme arbitraire. Nous présentons la sémantique formelle de SIAAM ainsi qu'une preuve d'isolation vérifiée avec l'assistant COQ. L'implantation du modèle de programmation pour le langage Java est réalisé dans la machine virtuelle JikesRVM. Enfin nous décrivons un ensemble d'analyses statiques qui réduit automatiquement le cout à l'exécution de notre approche.

Les langages synchrones tels que SIGNAL, LUSTRE et ESTEREL sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de SIGNAL. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé.

Ce mémoire d'habilitation résume la majeure partie de mes recherches, depuis la fin de mon doctorat, fin 2004, jusqu'à aujourd'hui. Le but essentiel de mes recherches est le développement de méthodes fondées sur des bases mathématiques et performantes en pratique pour s'assurer de la correction des logiciels. J'utilise des approximations pour permettre une bonne performance, tandis que la validité des résultats est garantie par l'emploi exclusif de sur-approximations des ensembles des comportements des programmes. Ma recherche est basée sur l'interprétation abstraite, une théorie très puissante des approximations de sémantiques permettant aisément de les développer, les comparer, les combiner. Je m'emploie en particulier au développement de nouveaux composants réutilisables d'abstraction, les domaines abstraits, qui sont directement implantables en machine, ainsi qu'à leur utilisation au sein d'analyseurs statiques, qui sont des outils de vérification automatique de programmes. Mes premières recherches concernaient l'inférence de propriétés numériques de programmes séquentiels, tandis que mes recherches actuelles se tournent vers l'analyse de programmes concurrents, d'où le titre de ce mémoire. Les deux premiers chapitres de ce mémoire constituent une introduction, tandis que les suivants présentent mon travail d'habilitation proprement dit. Le premier chapitre est une introduction informelle à la problématique de l'analyse de programmes, aux méthodes existantes, leurs forces et leurs faiblesses. Le deuxième chapitre présente de manière formelle les outils dont nous aurons besoin par la suite : les bases de l'interprétation abstraite, quelques domaines abstraits existants et la construction d'analyses statiques par interprétation abstraite, ainsi que quelques résultats utiles que j'ai obtenu en doctorat. Le troisième chapitre est consacré aux aspects spécifiques de l'analyse de programmes concurrents. Cette recherche, très personnelle, a abouti à la construction d'une méthode d'analyse de programmes concurrents, paramétrée par le choix de domaines abstraits, et basée sur une notion d'interférence abstrayant les interactions entre threads. Ainsi, l'analyse construite est modulaire pour les threads. Cette méthode est reliée aux preuves rely-guarantee proposées par Jones, ce que nous montrons formellement dans une première partie. Nous construisons ensuite une analyse à grands pas basée sur les interférences, efficace et facile à implanter. Les deux dernière parties étudient les liens entre l'analyse et les modèles mémoires faiblement cohérents (désormais incontournables) ainsi que le raffinement de l'analyse pour tenir compte des propriétés spécifiques des ordonnanceurs temps-réels (nous étudions en particulier l'effet des priorités des threads et l'emploi d'objets de synchronisation). Le quatrième et le cinquième chapitres sont consacrés à la constructions de domaines abstraits. Ceux-ci ne sont pas spécifiquement liés au problème de la concurrence ; ils sont utiles à l'analyse de tous programmes, séquentiels comme concurrents. Le chapitre 4 étudie des domaines numériques inférant des égalités et inégalités affines, développés en collaboration avec Liqian Chen, alors doctorant en visite à l'ENS. La motivation première était l'emploi de nombres à virgule flottante afin d'améliorer l'efficacité du domaine des polyèdres, mais ces travaux ont également débouché sur la découverte de nouveaux domaines, basés sur les relations affines à coefficients intervalles, que nous présentons également. Le chapitre 5 étudie les abstractions de types de données réalistes, comme ceux rencontrés dans le langage C : les entiers machines, les nombres à virgule flottante, et les blocs structurés (tableaux, structures, unions). Nos abstractions modélisent finement les détails de l'encodage en mémoire des données afin de permettre l'analyse de programmes qui en dépendent (par exemple, ceux utilisant le type-punning). Ces abstractions sont motivées par nos expériences d'analyses, avec les outils Astrée et AstréeA, de programmes C industriels ; ceux-ci employant fréquemment ce type de constructions de bas niveau. Le sixième chapitre est consacré aux applications des méthodes présentées ci-dessus à la construction d'outils d'analyse statique. Il décrit en particulier mon travail sur l'outil Astrée que j'ai co-développé avec l'équipe Abstraction pendant et après mon doctorat, et qui a été industrialisé en 2009. Mes résultats théoriques et appliqués ont contribué au succès d'Astrée, tandis que celui-ci m'a fourni de nouveaux thèmes de recherches, sous la forme de problèmes concrets dont la résolution n'a pu se faire que grâce à des développements théoriques. Ce chapitre décrit également AstréeA, une extension d'Astrée utilisant l'abstraction d'interférences proposée plus haut pour l'analyse de programmes concurrents (Astrée étant limité aux programmes séquentiels). Il décrit également Apron, une bibliothèque de domaines abstraits numériques que j'ai co-développée. Il s'agit d'un outil plus académique, dont le but est d'encourager la recherche sur les domaines numériques abstraits. Le mémoire se conclue par quelques perspectives sur des recherches futures.

Dans ce mémoire, nous proposons une solution possible à la question suivante : comment formaliser des environnements associés à un processus (quelconque) et comment utiliser les informations qu'ils contiennent pour produire des actions pertinentes ? Cette question nous a amené à introduire la notion de contexte ainsi qu'une représentation réutilisable des connaissances pour le formaliser. Nous nous sommes donc intéressés aux notions d'ontologies, de contextes et d'actions. Pour la représentation et le raisonnement sur les contextes et les actions, nous proposons une solution appelée DTF. Celle-ci étend une théorie constructive des types existante permettant ainsi de disposer d'une grande expressivité, de la décidabilité de la véri cation de types et d'un mécanisme de sous-typage e cace. Nous montrons comment modéliser les contextes et les actions sous la forme de types dépendants à partir des données fournies sur un problème et des actions à entreprendre pour le résoudre. En n, pour tester la faisabilité et pouvoir juger de la complexité d'une telle solution, un "démonstrateur de contexte " est réalisé avec un langage fonctionnel. Puis, une application test appelée " le monde du Wumpus " où un agent logiciel se déplace dans un environnement inconnu, est alors implantée en LISP.

Ce document présente l'étude de plusieurs modèles de machines à états finis qui étendent tous le même formalisme: les automates d'arbres classiques, et leur application dans différentes tâches telles que l'analyse statique de programmes ou de systèmes, la typage, la vérification de la cohérence de spécifications, le model checking... Les arbres sont une structure naturelle de données, très répandue en informatique, par exemple pour la représentation des structures de données hiérarchiques ou imbriquées, pour des algorithmes spécifiques (arbres binaires de recherche, algorithmes distribués), comme modèle abstrait pour des données semi-structurées utilisées pour l'échange d'information dans le Web, pour une présentation algébrique de processus récursifs, comme les termes en logique... Lorsqu'il s'agit de raisonner sur des systèmes manipulant des arbres, ou modelisés par des arbres, il est crucial d'avoir une représentation finie d'ensembles infinis d'arbres. Les automates d'arbres sont des machines à états finis permettant une telle représentation. Ils ont fait la preuve de leur adéquation à des tâches de raisonnement: ils ont un modèle théorique bien établi, en étroite relation avec la logique, ils bénéficient de bonnes propriétés de composition et d'algorithmes de décision efficaces. En particulier, les automates d'arbres sont utilisées au coeur de systèmes de vérification formelle d'outils de déduction automatique. Toutefois, les automates d'arbres ont des limitations sévères en expressivité. Par exemple, ils sont incapables de faire du filtrage non-linéaire ou d'exprimer des contraintes d'intégrité tels que les clés dans les bases de données. Certaines extensions ont été proposées afin d'améliorer le modèle en essayant de conserver de bonnes propriétés. Nous présentons dans ce document de plusieurs de telles extensions, leurs propriétés et leur utilisation en vérification symbolique de systèmes et de programmes.

Ce travail présente des contributions théoriques et appliquées dans le contexte des systèmes dynamiques discrets vus comme modèles des réseaux de régulation biologique. En mettant en avant le fait qu'accroître les connaissances du vivant nécessite aujourd'hui de mieux comprendre les propriétés mathématiques qui le régissent, il développe diverses réflexions menées en bio-informatique théorique en se fondant sur le formalisme des réseaux d'automates, notamment booléens. Les trois principaux thèmes abordés sur ces réseaux sont la robustesse environnementale, la combinatoire comportementale et la robustesse structurelle. La robustesse environnementale est notamment évoquée à travers une étude de la manière dont les réseaux d'automates réagissent face à l'influence de conditions de bord fixées (on y retrouve une généralisation au cas non-linéaire d'un résultat connu dans le domaine des automates cellulaires). La combinatoire comportementale est quant à elle abordée par les cycles d'interaction dont on connaît l'importance sur la dynamique des réseaux. Pour ces motifs particuliers et leurs intersections sont présentées des caractérisations combinatoires de leur comportement asymptotique en parallèle, qui font ensuite l'objet de comparaisons. Enfin, le thème de la robustesse structurelle est traité au travers du concept de graphe de transition général, qui a mené à mettre en évidence tous les comportements possibles des cycles d'interaction, à donner une classification de la robustesse des réseaux vis-à-vis de leur asynchronisme/synchronisme, de laquelle se sont imposées des études plus précises sur le rôle de la non-monotonie dans ces réseaux.