Les langages synchrones sont apparus autour des années quatre-vingt, en réponse à un besoin d'avoir un modèle mathématique simple pour implémenter des systèmes temps réel critiques. Dans ce modèle, le temps est découpé en instants discrets durant lesquels tous les composants du système reçoivent et produisent une donnée. Cette modélisation permet des raisonnements beaucoup plus simples en évitant de devoir prendre en compte le temps de calcul de chaque opération. Dans le monde du logiciel critique, la fiabilité du matériel et de son fonctionnement sont primordiaux, et on accepte d'être plus lent si on devient plus sûr. Afin d'augmenter cette fiabilité, plutôt que de concevoir manuellement tout le système, on utilise des machines qui synthétisent automatiquement le système souhaité à partir d'une description la plus concise possible. Dans le cas du logiciel, ce mécanisme s'appelle la compilation, et évite des erreurs introduites par l'homme par inadvertance. Elle ne garantit cependant pas la bonne correspondance entre le système produit et la description donnée. Des travaux récents menés par une équipe INRIA dirigée par Xavier Leroy ont abouti en 2008 au compilateur CompCert d'un sous-ensemble large de C vers l'assembleur PowerPC pour lequel il a été prouvé dans l'assistant de preuve Coq que le code assembleur produit correspond bien à la description en C du programme source. Un tel compilateur offre des garanties fortes de bonne correspondance entre le système synthétisé et la description donnée. De plus, avec les compilateurs utilisés pour le temps réel critique, la plupart des optimisations sont désactivées afin d'éviter les erreurs qui y sont liées. Dans CompCert, des optimisations elles aussi prouvées sont proposées, ce qui pourrait permettre ces passes dans la production de systèmes temps réel critiques sans en compromettre la fiabilité. Le but de cette thèse est d'avoir une approche similaire mais spécifique à un langage synchrone, donc plus approprié à la description de systèmes temps réel critiques que ne l'est le C. Un langage synchrone flots de données semblable à Lustre, nommé Ls, et un langage impératif semblable au langage C, nommé Obc y sont proposés ainsi que leur sémantique formelle et une chaîne de compilation avec des preuves de préservation de sémantique le long de cette chaîne.

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Actuellement, le développement d’un logiciel de taille industriel repose généralement surdes tests ou des preuves unitaires pour garantir rigoureusement ses exigences. En outre, il adéjà été montré que l’utilisation combinée du test et de la preuve unitaires est plus efficaceque l’utilisation d’une seule de ces deux techniques. Néanmoins, un ingénieur en vérificationhésite encore à utiliser ces deux techniques conjointement, faute d’une notion de couverturecommune au test et à la preuve. Définir une telle notion est l’objet de cette thèse.En effet, nous introduisons une nouvelle couverture, appelée « couverture label-mutant ».Elle permet de représenter les critères de couverture structurelle habituels du test, comme lacouverture des instructions, la couverture des branches ou la couverture MC/DC et de décidersi le critère choisi est satisfait en utilisant une technique de vérification formelle, qu’elle soitpar test, par preuve ou par une combinaison des deux. Elle permet également de représenterles critères de couverture fonctionnelle. Nous introduisons aussi dans cette thèse une méthodereposant sur des outils automatiques de test et de preuve pour réduire l’effort de vérificationtout en satisfaisant le critère de couverture choisi. Cette méthode est mise en oeuvre au seinde la plateforme d’analyse de code C (Frama-C), fournissant ainsi à un ingénieur un moyenopérationnel pour contrôler et réaliser la vérification qu’il souhaite. / Currently, industrial-strength software development usually relies on unit testing or unitproof in order to ensure high-level requirements. Combining these techniques has already beendemonstrated more effective than using one of them alone. The verification engineer is yetnot been to combine these techniques because of the lack of a common notion of coverage fortesting and proving. Defining such a notion is the main objective of this thesis.We introduce here a new notion of coverage, named « label-mutant coverage ». It subsumesmost existing structural coverage criteria for unit testing, including statement coverage,branch coverage or MC/DC coverage, while allowing to decide whether the chosen criterionis satisfied by relying on a formal verification technique, either testing or proving or both.It also subsumes functional coverage criteria. Furthermore, we also introduce a method thatmakes use of automatic tools for testing or proving in order to reduce the verification costwhile satisfying the chosen coverage criterion. This method is implemented inside Frama-C, aframework for verification of C code (Frama-C). This way, it offers to the engineer a way tocontrol and to perform the expected verifications.

Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux critères suivantes: puissance d'expression et décidabilité. Cette étude porte essentiellement sur fa comparaison des logiques du temps arborescent et des logiques du temps linéaire. Ensuite, le problème de l'utilisation des logiques du temps arborescent en tant qu'outils de preuves des programmes est étudié. Nous proposons une logique pour la preuve constructive des propriétés des processus contrôlables de CCS. Cette logique est telle, que la relation de congruence induite est la congruence observationnelle de CCS

Nous nous intéressons ici à la génération de programmes certifiés<br />corrects par construction. Ces programmes sont obtenus en<br />extrayant l'information pertinente de preuves constructives réalisées<br />dans l'assistant de preuves Coq.<br /><br />Une telle traduction, ou "extraction", des preuves constructives<br />en programmes fonctionnels n'est pas nouvelle, elle correspond <br />à un isomorphisme bien connu sous le nom de Curry-Howard. Et<br />l'assistant Coq comporte depuis longtemps un tel outil d'extraction. <br />Mais l'outil précédent présentait d'importantes limitations. Certaines <br />preuves Coq étaient ainsi hors de son champ d'application, alors que <br />d'autres engendraient des programmes incorrects.<br /><br />Afin de résoudre ces limitations, nous avons effectué une refonte<br />complète de l'extraction dans Coq, tant du point de vue de la théorie<br />que de l'implantation. Au niveau théorique, cette refonte a entraîné<br />la réalisation de nouvelles preuves de correction de ce mécanisme<br />d'extraction, preuves à la fois complexes et originales. Concernant<br />l'implantation, nous nous sommes efforcés d'engendrer du code <br />extrait efficace et réaliste, pouvant en particulier être intégré dans des<br />développement logiciels de plus grande échelle, par le biais de<br />modules et d'interfaces.<br /><br />Enfin, nous présentons également plusieurs études de cas illustrant<br />les possibilités de notre nouvelle extraction. Nous décrivons ainsi la<br />certification d'une bibliothèque modulaire d'ensembles finis, et <br />l'obtention de programmes d'arithmétique réelle exacte à partir d'une <br />formalisation d'analyse réelle constructive. Même si des progrès <br />restent encore à obtenir, surtout dans ce dernier cas, ces exemples <br />mettent en évidence le chemin déjà parcouru.

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L'approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l'industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d'étude, qui s'inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d'une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d'écrire des programmes structurés en composants. L'introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d'alias, on risque de ne plus pouvoir garantir la validité de l'invariant de données d'une structure. Nous interdisons, alors l'aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s'inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d'obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d'obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s'apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu'aucun invariant de données n'est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l'affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d'un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires.

Les langages synchrones sont apparus autour des années quatre-vingt, en réponse à un besoin d’avoir un modèle mathématique simple pour implémenter des systèmes temps réel critiques. Dans ce modèle, le temps est découpé en instants discrets durant lesquels tous les composants du système reçoivent et produisent une donnée. Cette modélisation permet des raisonnements beaucoup plus simples en évitant de devoir prendre en compte le temps de calcul de chaque opération. Dans le monde du logiciel critique, la fiabilité du matériel et de son fonctionnement sont primordiaux, et on accepte d’être plus lent si on devient plus sûr. Afin d’augmenter cette fiabilité, plutôt que de concevoir manuellement tout le système, on utilise des machines qui synthétisent automatiquement le système souhaité à partir d’une description la plus concise possible. Dans le cas du logiciel, ce mécanisme s’appelle la compilation, et évite des erreurs introduites par l’homme par inadvertance. Elle ne garantit cependant pas la bonne correspondance entre le système produit et la description donnée. Des travaux récents menés par une équipe INRIA dirigée par Xavier Leroy ont abouti en 2008 au compilateur CompCert d’un sous-ensemble large de C vers l’assembleur PowerPC pour lequel il a été prouvé dans l’assistant de preuve Coq que le code assembleur produit correspond bien à la description en C du programme source. Un tel compilateur offre des garanties fortes de bonne correspondance entre le système synthétisé et la description donnée. De plus, avec les compilateurs utilisés pour le temps réel critique, la plupart des optimisations sont désactivées afin d’éviter les erreurs qui y sont liées. Dans CompCert, des optimisations elles aussi prouvées sont proposées, ce qui pourrait permettre ces passes dans la production de systèmes temps réel critiques sans en compromettre la fiabilité. Le but de cette thèse est d’avoir une approche similaire mais spécifique à un langage synchrone, donc plus approprié à la description de systèmes temps réel critiques que ne l’est le C. Un langage synchrone flots de données semblable à Lustre, nommé Ls, et un langage impératif semblable au langage C, nommé Obc y sont proposés ainsi que leur sémantique formelle et une chaîne de compilation avec des preuves de préservation de sémantique le long de cette chaîne. / Synchronous languages first appeared during the 80’s, in order to provide a mathematical model for safety-critical systems. In this model, time is discrete. At each instant, all components of the system simultaneously receive and produce some data. This model allows simpler reasonning on the behaviour of the system, as it does not involve the time required for each of the operations for every component. In safety-critical systems, safety is the rule, so a poor performance behaviour can be allowed if it improves safety. In order to improve safety, rather than conceiving directly the system, machines are used to automatically design the system from a given concise description. In the case of software, this machine is called a compiler, and avoids issues due to some human inadvertence. But it does not ensure that the produced system and the description specification really show the same behaviour. Some recent work from an INRIA team lead by Xavier Leroy achieved in 2008 the realisation of the CompCert compiler from a large subset of C to PowerPC assembly, for which it was proven inside of the Coq proof assistant that the produced system fits its source description. Such a compiler offers strong guarantees that the produced system and its given description by the programmer really fit. Furthermore, most current compiler’s optimizations are disabled when dealing with safety-critical systems in order to avoid tedious compilation errors that optimizations may introduce. Proofs for optimizations may allow their use in this domain without affecting the faith we could place in the compiler. The aim of this thesis is to follow a similar path, but this one on a language which would be more suited for safety-critical systems than the C programming language. Some dataflow synchronous programming language very similar to Lustre, called Ls is described with its formal semantics, as well as an imperative programming language similar to a subset of C called Obc. Furthermore some compilation process is described as well as some proofs that the semantics is preserved during the compilation process.

Le problème général de la preuve de propriétés de programmes impératifs est indécidable. Pour deslangages de programmation et de propriétés plus restrictifs, des sous-problèmes décidables sontconnus. En pratique, grâce à des heuristiques, les outils de preuve de programmes automatisent despreuves qui sortent du cadre théorique de ces sous-problèmes décidables connus. Nous illustronscette réussite pratique en construisant un catalogue de preuves, pour des programmes et despropriétés de nature similaire et de complexité croissante. Ces programmes sont principalementdes générateurs de cartes combinatoires.Ainsi, ce travail contribue aux domaines de recherche de la combinatoire énumérative et dugénie logiciel. Nous distribuons une bibliothèque C de générateurs exhaustifs bornés de tableauxstructurés, formellement spécifiés en ACSL et vérifiés avec le greffon WP de la plateforme d’analyseFrama-C. Nous proposons également une méthodologie de test qui facilite la preuve interactive enCoq, une étude formelle des cartes originale, et de nouveaux résultats en combinatoire énumérative. / The general problem of proving properties of imperative programs is undecidable. Some subproblems– restricting the languages of programs and properties – are known to be decidable. Inpractice, thanks to heuristics, program proving tools sometimes automate proofs for programs andproperties living outside of the theoretical framework of known decidability results. We illustrate thisfact by building a catalog of proofs, for similar programs and properties of increasing complexity. Mostof these programs are combinatorial map generators.Thus, this work contributes to the research fields of enumerative combinatorics and softwareengineering. We distribute a C library of bounded exhaustive generators of structured arrays, formallyspecified in ACSL and verified with the WP plugin of the Frama-C analysis platform. We also proposea testing-based methodology to assist interactive proof in Coq, an original formal study of maps, andnew results in enumerative combinatorics.

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L’approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l’industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d’étude, qui s’inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d’une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d’écrire des programmes structurés en composants. L’introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d’alias, on risque de ne plus pouvoir garantir la validité de l’invariant de données d’une structure. Nous interdisons, alors l’aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s’inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d’obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d’obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s’apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu’aucun invariant de données n’est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l’affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d’un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires. / The purpose of this thesis is to specify and prove programs with pointers, such as C programs, using refinement techniques. The proposed approach allows a compromise between the complexe methods that exist in the literature and what is used in industry, reconciling lightness annotations and restrictions on the alias. We define, firstly, a language study, based on the C language, in which the only type of mutable data allowed is the type of structures, which can be accessed only through pointers. In order to structure our programs, we bring our language with a module notion and concepts issue from a refinement theory such as abstract variables that we formalize by model fields and gluing invariants. This allows us to write programs structured by components. Introducing invariants in our language raises issues related to aliasing. Indeed, in presence of alias, we might not be able to guarantee the validity of the invariant data structure. We forbid then the aliasing in our language. To control memory access, we define a type system based on the concept of regions. This contribution is based on the theory and refinement. It aims to make programs as modular as possible and proofs as automatic as possible. We define on this language, a mechanism for generation of proof obligations by proposing a weakest precondition calculus incorporating refinement. Next we prove the correction of this proof obligations generation mechnaism by an original method based on the concept of blocking semantic, which is similar to a proof of type soundness, and consists therefore, to proove the preservation and the progress of the defined calculus. Secondly, we extend our language by, partially, lifting the restrictions related to aliasing. We allow, in particular, sharing when no invariant is associated to the referenced data structure. In addition, we introduce the type of arrays, global variables, and assignment that are not part of the core language. For each of the extensions mentioned above, we extend the definition and correctness proof of the weakest precondition calculus accordingly. Finally, we propose an implementation of this approach as a Frama-C plugin(http ://frama-c.com/). We experimente our implantation on examples of modules implementing complex data structures, especially the challenges from the challenge VACID0 (http ://vacid. Codeplex.com /), namely sparse srrays and binary heaps.