L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type. / Formal methods are rapidly improving and gaining ground in software. Type systems are the most successful and popular formal method used to develop software. As the technology of type systems progresses, new needs and new opportunities appear. One of those needs is to ensure the faithfulness of the translation from source code to machine code, so that the properties you prove about the code you write also apply to the code you run. This thesis presents a compiler from a polymorphic higher-order functional language to typed assembly language, whose main property is that type preservation is verified statically, through type annotations on the compiler's code. Our compiler implements the essential code transformations for a higher-order functional language, namely a CPS conversion and closure conversion as well as a code generation. The thesis presents the details of the strongly typed intermediate representations and the constraints they set on the implementation of code transformations. Our goal is to guarantee type preservation with a minimum of type annotations, and without compromising readability and modularity of the code. This goal is already a reality for simple types, and we discuss the problems remaining for polymorphism, which still requires substantial extra work to satisfy the type checker.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Des nombreuses applications de méthodes formelles se fondent sur les solveurs SMT pour valider automatiquement les conditions à vérifier et fournissent des certificats de leurs résultats. Nous visons à la fois à améliorer l'efficacité des solveurs SMT et à accroître leur fiabilité. Notre première contribution est un cadre uniforme pour le raisonnement avec des formules quantifiées dans les solveurs SMT, dans lequel généralement diverses techniques d'instanciation sont utilisées. Nous montrons que les principales techniques d'instanciation peuvent être jetées dans ce cadre. Le cadre repose sur le problème de l'E-ground (dis)unification. Nous présentons une procédure de décision pour résoudre ce problème en pratique: Fermeture de congruence avec variables libres (CCFV}). Nous mesurons l'impact de CCFV dans les solveurs SMT veriT et CVC4. Nous montrons que nos implémentations présentent des améliorations par rapport aux approches à la fine pointe de la technologie. Notre deuxième contribution est un cadre pour le traitement des formules tout en produisant des preuves détaillées. Les principaux composants de notre cadre de production de preuve sont un algorithme de récurrence contextuelle générique et un ensemble extensible de règles d'inférence. Avec des structures de données appropriées, la génération des preuves ne crée que des frais généraux linéaires et les vérifications peuvent être vérifiées en temps linéaire. Nous avons également mis en œuvre l'approche en veriT. Cela nous a permis de simplifier considérablement la base du code tout en augmentant le nombre de problèmes pour lesquels des preuves détaillées peuvent être produites / In many formal methods applications it is common to rely on SMT solvers to automatically discharge conditions that need to be checked and provide certificates of their results. In this thesis we aim both to improve their efficiency of and to increase their reliability. Our first contribution is a uniform framework for reasoning with quantified formulas in SMT solvers, in which generally various instantiation techniques are employed. We show that the major instantiation techniques can be all cast in this unifying framework. Its basis is the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduce a decision procedure to solve this problem in practice: Congruence Closure with Free Variables (CCFV). We measure the impact of optimizations and instantiation techniques based on CCFV in the SMT solvers veriT and CVC4, showing that our implementations exhibit improvements over state-of-the-art approaches in several benchmark libraries stemming from real world applications. Our second contribution is a framework for processing formulas while producing detailed proofs. The main components of our proof producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. With suitable data structures, proof generation creates only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced

La méthodologie HILECOP a été élaborée pour la conception formelle de systèmes numériques complexes critiques ; elle couvre donc l'intégralité du processus, allant de la modélisation à la génération de code pour l’implantation sur la cible matérielle (composant électronique de type FPGA), en passant par la validation formelle. Or, si le modèle formel, les réseaux de Petri en l'occurrence, est par essence asynchrone, il est néanmoins exécuté de manière synchrone sur la cible. De fait, les approches d'analyse usuelles ne sont pas adaptées au sens où elles construisent des graphes d'états non conformes à l'évolution d'états réelle au sein de la cible. Dans l'objectif de gagner en confiance quant à la validité des résultats de l’analyse formelle, ces travaux visent à capturer les caractéristiques dites non-fonctionnelles, à les réifier sur le modèle et enfin à considérer leur impact à travers l’analyse. En d’autres termes, l’objectif est d’améliorer l’expressivité du modèle et la pertinence de l'analyse, en considérant des aspects comme la synchronisation d'horloge, le parallélisme effectif, le risque de blocage induit par l'expression conjointe d'un événement (condition) et d'une fenêtre temporelle d'occurrence, sans omettre la gestion des exceptions. Pour traiter tous ces aspects, nous avons proposé une nouvelle méthode d'analyse pour les réseaux de Petri temporels généralisés étendus interprétés exécutés en synchrone, en les transformant vers un formalisme équivalent analysable. Ce formalisme est associé avec une sémantique formelle intégrant toutes les aspects particuliers de l'exécution et un algorithme de construction d'un graphe d'états spécifique : le Graphe de Comportement Synchrone. Nos travaux ont été appliqués à un cas industriel, plus précisément à la validation du comportement de la partie numérique d'un neuro-stimulateur. / The HILECOP methodology has been developed for the formal design of critical complex digital systems; it therefore covers the entire design process, ranging from modeling to code generation for implementation on the hardware target (FPGA type electronic component), via formal validation. However, if the formal model, the Petri nets in this case, is inherently asynchronous, it is nevertheless executed synchronously on the target. In fact, the usual analysis approaches are not adapted in the sense that they construct state graphs that do not conform to the real state evolution within the target. In order to gain confidence in the validity of the results of the formal analysis, this work aims to capture the so-called non-functional characteristics, to reify them on the model and finally to consider their impact through the analysis.In other words, the aim is to improve the expressiveness of the model and the relevance of the analysis, considering aspects such as clock synchronization, effective parallelism, the risk of blocking induced by the expression of an event (condition) and a time window of occurrence, without omitting the management of exceptions.To deal with all these aspects, we have proposed a new method of analysis for extended generalized synchronous executed time Petri nets, transforming them into an analysable equivalent formalism. This formalism is associated with a formal semantics integrating all the particular aspects of the execution and dédicated state space construction algorithm: the Synchronous Behavior Graph.Our work has been applied to an industrial case, more precisely to the validation of the behavior of the digital part of a neuro-stimulator.

Le travail présenté dans ce mémoire concerne une méthode de conception sûre de systèmes(COTS). Un COTS est un composant matériel ou logiciel générique qui est naturellement conçu pour être réutilisable et cela se traduit par une forme de flexibilité dans la mise en oeuvre de sa fonctionnalité : en clair, une même fonction peut être réalisée par un ensemble (potentiellement infini) de scénarios différents, tous réalisables par le COTS. La complexité grandissante des fonctions implémentées fait que ces situations sont très difficiles à anticiper d’une part, et encore plus difficiles à éviter par un codage correct. Réaliser manuellement une fonction composite correcte sur un système de taille industrielle, s’avère être très coûteuse. Elle nécessite une connaissance approfondie du comportement des COTS assemblés. Or cette connaissance est souvent manquante, vu qu’il s’agit de composants acquis, ou développés par un tiers, et dont la documentation porte sur la description de leur fonction et non sur sa mise en IJuvre. Par ailleurs, il arrive souvent que la correction manuelle d’une faute engendre une ou plusieurs autres fautes, provoquant un cercle vicieux difficile à maîtriser. En plus, le fait de modifier le code d’un composant diminue l’avantage lié à sa réutilisation. C’est dans ce contexte que nous proposons l’utilisation de la technique de synthèse du contrôleur discret (SCD) pour générer automatiquement du code de contrôle commande correct par construction. Cette technique produit des composants, nommés contrôleurs, qui agissent en contraignant le comportement d’un (ou d’un assemblage de) COTS afin de garantir si possible la satisfaction d’une exigence fonctionnelle. La méthode que nous proposons possède plusieurs étapes de conception. La première étape concerne la formalisation des COTS et des propriété de sûreté et de vivacité (P) en modèles automate à états et/ou en logique temporelle. L’étape suivante concerne la vérification formelle du modèle d’un(des) COTS pour l’ensemble des propriétés (P). Cette étape découvrir les états de violation des propriétés (P) appelés états d’erreur. La troisième étape concerne la correction automatique des erreurs détectées en utilisant la technique SCD. Dans cette étape génère on génère un composant correcteur qui sera assemblé au(x) COTS original(aux) pour que leur comportement général respecte les propriétés souhaitées. L’étape suivante concerne la vérification du système contrôlé pour un ensemble de propriétés de vivacité pour assurer la passivité du contrôleur et la vivacité du système. En fin, une étape de simulation est proposée pour observer le comportement du système pour quelque scénarios intéressent par rapport à son implémentation finale. / This PhD dissertation contributes to the safe design of COTS-based control-command embedded systems. Due to design constraints bounding delays, costs and engineering resources, component re-usability has become a key issue in embedded design. Our proposal is a design method which ensures correction of COTS-based designs. This method uses in synergy a number of design techniques and tools. It starts from modeling of the COTS components which are stored in a generic COTS library, and ends with a design of the global control-command system, verified to be free of errors and ready to be implemented over a hardware chip such as an ASIC or an FPGA "Field Programmable Gate Array". The designer starts by modeling the temporal and logical local preconditions and postconditions of each COTS component, then the global pre/post conditions of the assembly which are not necessary a simple combination of local properties. He models also a list of properties that must be satisfied by the assembly. Any violation of these properties is defined as a design error. Then, by using the model checking approach the model of the assembly is verified against the predefined local and global properties. Some design errors can be corrected automatically through the Discrete Controller Synthesis method (DCS), others however must be manually corrected. After the correction step, the controlled control-command system is verified. Finally a global simulation step is proposed in order to perform a system-level verification beyond the capabilities of available formal tools. We apply the method on two different systems, one concerns transferring data from senders to receivers through FIFO unit, the other is controlcommand system of a train passengers’ access.

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL. / The work in this thesis is at the intersection of two major research domains~: Model-Driven Engineering (MDE) and formal methods, and has various fields of application. This thesis deals with the formal verification of parallel applications modelled by the MDE approach. In this approach, models play a central role and enable to develop an application through successive transformations (automated or not) between intermediate models of differing levels of abstraction, until executable code is produced. When models have a formal semantics, the application can be verified, either automatically or semi-automatically. These principles are used in TOPCASED, an ECLIPSE-based development environment for critical embedded applications, which enables formal verification by interconnecting existing tools. This thesis implements the TOPCASED approach by relying on the CADP toolbox for verifying systems, and on its most recent input formalism : LOTOS NT. This thesis tackles the formal verification of MDE applications through two real problems : 1) For GALS (Globally Asynchronous, Locally Synchronous), a generic verification method, based on a transformation to LOTOS NT, is proposed and illustrated by an industrial case-study provided by AIRBUS : a communication protocol between the airplane and the ground described in the synchronous langage SAM designed at AIRBUS. 2) For Web services specified with the BPEL (Business Process Execution Language) norm, a verification method is proposed. It is based on a BPEL to LOTOS NT transformation which takes into account XML Schema, Xpath, and WSDL, the languages on which the BPEL norm is built.

Les attaques par canaux cachés sont une forme d'attaque particulièrement dangereuse. Dans cette thèse, nous nous intéressons au canal caché temporel. Un programme est dit ''constant-time'' lorsqu'il n'est pas vulnérable aux attaques par canal caché temporel. Nous présentons dans ce manuscrit deux méthodes reposant sur l'analyse statique afin de s'assurer qu'un programme est constant-time. Ces méthodes se placent dans le cadre de vérification formelle afin d'obtenir le plus haut niveau d'assurance possible en s'appuyant sur une chaîne de compilation vérifiée composée du compilateur CompCert et de l'analyseur statique Verasco. Nous proposons aussi une méthode de preuve afin de s'assurer qu'un compilateur préserve la propriété de constant-time lors de la compilation d'un programme. / Side-channel attacks are an especially dangerous form of attack. In this thesis, we focus on the timing side-channel. A program is said to be constant-time if it is not vulnerable to timing attacks. We present in this thesis two methods relying on static analysis in order to ensure that a program is constant-time. These methods use formal verification in order to gain the highest possible level of assurance by relying on a verified compilation toolchain made up of the CompCert compiler and the Verasco static analyzer. We also propose a proof methodology in order to ensure that a compiler preserves constant-time security during compilation.

Les réseaux de régulation génique contrôlent le développement et le fonctionnement des organismes vivants. Etant donné que la plupart des réseaux de régulation génique d'intérêt biologique sont grands et que leur dynamique est complexe, la compréhension de leur fonctionnement est un problème biologique majeur. De nombreuses méthodes ont été développées pour la modélisation et la simulation de ces systèmes. Etonnamment, le problème de la validation de modèle n'a reçu jusqu'à récemment que peu d'attention. Pourtant, cette étape est d'autant plus importante que dans le contexte de la modélisation de réseaux de régulation génique, les systèmes modélisés sont complexes et encore imparfaitement connus.<br /><br />Dans cette thèse, nous proposons une approche permettant de tester la validité de modèles de réseaux de régulation génique en comparant les prédictions obtenues avec les données expérimentales. Plus spécifiquement, nous considérons dans ce travail une classe de modèles qualitatifs définis en termes d'équations différentielles linéaires par morceaux (LPM). Ces modèles permettent de capturer les aspects essentiels des régulations géniques, tout en ayant une forme mathématique simple qui facilite leur analyse symbolique. Egalement, nous souhaitons utiliser les informations qualitatives sur la dynamique du système données par les changements du sens de variation des concentrations des protéines du réseau. Ces informations peuvent être obtenues expérimentalement à partir de profils d'expression temporels.<br /><br />La méthode proposée doit satisfaire deux contraintes. Premièrement, elle doit permettre d'obtenir des prédictions bien adaptées à la comparaison avec le type de données considéré. Deuxièmement, étant donné la taille et la complexité des réseaux d'intérêt biologique, la méthode doit également permettre de vérifier efficacement la cohérence entre prédictions et observations.<br /><br />Pour répondre à ces deux contraintes, nous étendons dans deux directions une approche précédemment développée par de Jong et collègues pour l'analyse symbolique des modèles LPM qualitatifs. Premièrement, nous proposons d'utiliser une représentation plus fine de l'état du système, permettant d'obtenir, par abstraction discrète, des prédictions mieux adaptées à la comparaison avec les données expérimentales. Deuxièmement, nous proposons de combiner cette méthode avec des techniques de model checking. Nous montrons que l'utilisation combinée d'abstraction discrète et de model checking permet de vérifier efficacement les propriétés dynamiques, exprimées en logique temporelle, des modèles continus.<br /><br />Cette méthode a été implémentée dans une nouvelle version de l'outil Genetic Network Analyzer (GNA 6.0). GNA 6.0 a été utilisé pour la validation de deux modèles grands et complexes de l'initiation de la sporulation chez <I>B. subtilis</I> et de la réponse au stress nutritionnel chez <I>E. coli</I>. Nous avons ainsi pu vérifier que les prédictions obtenues étaient en accord avec la plupart des données expérimentales disponibles dans la littérature. Plusieurs incohérences ont également été identifiées, suggérant des révisions des modèles ou la réalisation d'expériences complémentaires. En dehors d'une contribution à une meilleure compréhension du fonctionnement de ces systèmes, ces deux études de cas illustrent plus généralement que, par la méthode proposée, il est possible de tester si des prédictions obtenues pour des modèles complexes sont cohérentes avec un large éventail de propriétés observables expérimentalement.

L'Ingénierie Système (IS) est une méthodologie pluridisciplinaire de conception et de mise en oeuvre des systèmes complexes. La maîtrise de la Sûreté de Fonctionnement est un processus essentiel de l'IS et, dans sa poursuite, le recours à des méthodes formelles telles que le model checking se heurte généralement à des diffcultés d'utilisation. Dans cette thèse Cifre, effectuée en collaboration avec l'IRCCyN et Sodius, nous avons cherché à concevoir un outil de vérification formelle d'architectures fonctionnelles qui soit immédiatement utilisable dans des démarches de conception d'IS. Dans ce but, nous transformons des modèles et des propriétés comportementales haut niveau vers des équivalents bas niveau sur lesquels sont effectuées les vérifications formelles, le résultat étant présenté en termes haut niveau. Plus particulièrement, nous avons choisi comme modèles d'entrée les diagrammes EFFBDs : ils constituent un outil de modélisation largement utilisé en IS et adapté aux contraintes du model checking. Nous en avons établi la syntaxe et la sémantique formelles ; nous avons alors pu décrire une transformation vers les réseaux de Petri temporels (TPNs) dont nous avons prouvé qu'elle préserve le comportement temporel des modèles. Parallèlement, nous avons décrit une logique temporelle quantitative adaptée aux EFFBDs et sa traduction vers une logique correspondante sur les TPNs; nous avons alors pu établir la complexité de son model checking. Ces différents résultats théoriques nous ont ensuite permis de réaliser un outil de simulation enfin de vérification d'architectures fonctionnelles et dysfonctionnelles (c.-à-d. modélisant des fonctions défaillantes), déployé et utilisé industriellement.

La difficulté d'exprimer les propriétés formelles d'un contrôleur logique en vue de sa vérification est un des obstacles majeurs à la diffusion de ce type de techniques. L'objectif de cette thèse est donc de faciliter l'élaboration de ces propriétés formelles en proposant une méthode basée sur l'analyse prévisionnelle par Arbre des Défaillances (AdD). Ainsi, une propriété sera la non réalisation d'une faute. Quatre contributions sont alors développées pour mettre au point cette méthode : deux contributions de nature méthodologique et deux autres de nature formelle. Les contributions de la première catégorie sont, d'une part, l'intégration, dans la structure de l'AdD, des fautes du logiciel de commande du contrôleur logique (dites fautes systématiques car reproductibles) et, d'autre part, la représentation de ces fautes systématiques avec un vocabulaire de portes prenant en compte les temps logique et physique. Les deux contributions formelles proposent une sémantique formelle, en premier lieu, des portes adoptées dans le travail, et deuxièmement, d'associations de portes. Enfin, un exemple permet de montrer l'intérêt de ces quatre propositions pour l'amélioration de la sûreté des contrôleurs logiques.