Les systèmes embarqués ont évolué d'une manière spectaculaire et sont devenus partie intégrante de notre quotidien. En réponse aux exigences grandissantes en termes de nombre de fonctionnalités et donc de flexibilité, les parties logicielles de ces systèmes se sont vues attribuer une place importante malgré leur manque d'efficacité, en comparaison aux solutions matérielles. Par ailleurs, vu la prolifération des systèmes nomades et à ressources limités, tenir compte de la performance est devenu indispensable pour bien les concevoir. Dans cette thèse, nous proposons une démarche rigoureuse et intégrée pour la modélisation et l'évaluation de performance tôt dans le processus de conception. Cette méthode permet de construire des modèles, au niveau système, conformes aux spécifications fonctionnelles, et intégrant les contraintes non-fonctionnelles de l'environnement d'exécution. D'autre part, elle permet d'analyser quantitativement la performance de façon rapide et précise. Cette méthode est guidée par les modèles et se base sur le formalisme $mathcal{S}$BIP que nous proposons pour la modélisation stochastique selon une approche formelle et par composants. Pour construire des modèles conformes au niveau système, nous partons de modèles purement fonctionnels utilisés pour générer automatiquement une implémentation distribuée, étant donnée une architecture matérielle cible et un schéma de répartition. Dans le but d'obtenir une description fidèle de la performance, nous avons conçu une technique d'inférence statistique qui produit une caractérisation probabiliste. Cette dernière est utilisée pour calibrer le modèle fonctionnel de départ. Afin d'évaluer la performance de ce modèle, nous nous basons sur du model checking statistique que nous améliorons à l'aide d'une technique d'abstraction. Nous avons développé un flot de conception qui automatise la majorité des phases décrites ci-dessus. Ce flot a été appliqué à différentes études de cas, notamment à une application de reconnaissance d'image déployée sur la plateforme multi-cœurs STHORM. / In the present work, we tackle the problem of modeling and evaluating performance in the context of embedded systems design. These have become essential for modern societies and experienced important evolution. Due to the growing demand on functionality and programmability, software solutions have gained in importance, although known to be less efficient than dedicated hardware. Consequently, considering performance has become a must, especially with the generalization of resource-constrained devices. We present a rigorous and integrated approach for system-level performance modeling and analysis. The proposed method enables faithful high-level modeling, encompassing both functional and performance aspects, and allows for rapid and accurate quantitative performance evaluation. The approach is model-based and relies on the $mathcal{S}$BIP formalism for stochastic component-based modeling and formal verification. We use statistical model checking for analyzing performance requirements and introduce a stochastic abstraction technique to enhance its scalability. Faithful high-level models are built by calibrating functional models with low-level performance information using automatic code generation and statistical inference. We provide a tool-flow that automates most of the steps of the proposed approach and illustrate its use on a real-life case study for image processing. We consider the design and mapping of a parallel version of the HMAX models algorithm for object recognition on the STHORM many-cores platform. We explored timing aspects and the obtained results show not only the usability of the approach but also its pertinence for taking well-founded decisions in the context of system-level design.

Les circuits microélectroniques récents intègrent des dizaines d'horloges afin d'optimiser leur consommation et leur performance. Le nombre de traversées de domaines d'horloges (CDC) et la complexité des systèmes augmentant, garantir formellement l'intégrité d'une donnée devient un défi majeur. Plusieurs problèmes sont alors soulevés : configurer le système dans un mode réaliste, décrire l'environnement par des hypothèses sur les protocoles, gérer l'explosion de l'espace des états, analyser les contre-exemples, ...La première contribution de cette thèse a pour but d'atteindre une configuration complète et réaliste du système. Nous utilisons de la vérification formelle paramétrique ainsi qu'une analyse de la structure du circuit afin de détecter automatiquement les composants des arbres d'horloge. La seconde contribution cherche à éviter l'explosion de l'espace des états en combinant des abstractions localisées du circuit avec une analyse de contre-examples. L'idée clé est d'utiliser la technologie de raffinement d'abstraction guidée par contre-exemple (CEGAR) où l'utilisateur influence la poursuite de l'algorithme en se basant sur des informations extraites des contre-exemples intermédiaires. La troisième contribution vise à créer des hypothèses pour des environnements sous-contraints. Tout d’abord, plusieurs contre-exemples sont générés pour une assertion, avec différentes raisons d’échec. Ensuite, des informations en sont extraites et transformées en hypothèses réalistes.Au final, cette thèse montre qu'une vérification formelle concluante peut être obtenue en combinant la rapidité de l'analyse structurelle avec l'exhaustivité des méthodes formelles. / Modern hardware designs typically comprise tens of clocks to optimize consumption and performance to the ongoing tasks. With the increasing number of clock-domain crossings as well as the huge complexity of modern SoCs, formally proving the functional integrity of data propagation became a major challenge. Several issues arise: setting up the design in a realistic mode, writing protocol assumptions modeling the environment, facing state-space explosion, analyzing counter-examples, ...The first contribution of this thesis aims at reaching a complete and realistic design setup. We use parametric liveness verification and a structural analysis of the design in order to identify behaviors of the clock and reset trees. The second contribution aims at avoiding state-space explosion, by combining localization abstractions of the design, and counter-example analysis. The key idea is to use counterexample-guided abstraction refinement as the algorithmic back-end, where the user influence the course of the algorithm based on relevant information extracted from intermediate abstract counterexamples. The third contribution aims at creating protocol assumptions for under-specified environments. First, multiple counter-examples are generated for an assertion, with different causes of failure. Then, information is mined from them and transformed into realistic protocol assumptions.Overall, this thesis shows that a conclusive formal verification can be obtained by combining inexpensive structural analysis along with exhaustive model checking.

Cette thèse a pour cadre scientifique la décomposition formelle des spécifications centrali- sées Event-B appliquée aux systèmes distribués BIP. Elle propose une démarche descendante de développement des systèmes distribués corrects par construction en combinant judicieu- sement Event-B et BIP. La démarche proposée comporte trois étapes : Fragmentation, Dis- tribution et Génération de code BIP. Les deux concepts clefs Fragmentation et Distribution, considérés comme deux sortes de raffinement automatique Event-B paramétrées à l'aide de deux DSL appropriés, sont introduits par cette thèse. Cette thèse apporte également une contribution au problème de la génération de code à partir d'un modèle Event-B issu de l'étape de distribution. Nous traitons aussi bien les aspects architecturaux que comportemen- taux. Un soin particulier a été accordé à l'outillage et l'expérimentation de cette démarche. Pour y parvenir, nous avons utilisé l'approche IDM pour l'outillage et l'application Hôtel à clés électroniques pour l'expérimentation. / The scientific framework of this thesis is the formal decomposition of the centralized specifications Event-B applied to distributed systems based on the BIP (Behavior, Interaction, Priority) component framework. It suggets a top-down approach to the development of correct by construction distributed systems by judiciously combining Event-B and BIP. The proposed approach consists in three steps : Fragmentation, Distribution and Generation of BIP code. We introduce two key concepts, Fragmentation and Distribution, which are considered as two kinds of automatic refinement of Event-B models. They are parameterized using two appropriate DSL. This thesis also contributes to the problem of code generation from Event- B models resulting from the Distribution step. Accordingly, we deal with both architectural and behavioral aspects. A special care has been devoted to the implementation and the experimentation of this approach. To achieve this, we have used the IDM approach for tooling and the Electronic Hotel Key System for experimentation.

La mise à jour dynamique des programmes consiste en la modification de ceux-ci sans en arrêter l'exécution. Cette caractéristique est primordiale pour les applications critiques en continuelles évolutions et nécessitant une haute disponibilité. Le but de notre travail est d'effectuer la vérification formelle de la correction de la mise à jour dynamique d'applications Java Card à travers l'étude du système EmbedDSU. Pour ce faire, nous avons premièrement établi la correction de la mise à jour du code en définissant une sémantique formelle des opérations de mise à jour sur le code intermédiaire Java Card en vue d'établir la sûreté de typage des mises à jour. Nous avons ensuite proposé une approche pour vérifier la sémantique du code mis à jour à travers la définition d'une transformation de prédicats. Nous nous sommes ensuite intéressés à la vérification de la correction concernant la détection de points sûrs de la mise à jour. Nous avons utilisé la vérification de modèles. Cette vérification nous a permis de corriger d'abord un problème d'inter blocage dans le système avant d'établir d'autres propriétés de correction : la sûreté d'activation et la garantie de mise à jour. La mise à jour des données est effectuée à travers les fonctions de transfert d'état. Pour cet aspect, nous avons proposé une solution permettant d'appliquer les fonctions de transfert d’état tout en préservant la consistance du tas de la machine virtuelle Java Card et en permettant une forte expressivité dans leurs écritures. / Dynamic Software Updating (DSU) consists in updating running programs on the fly without any downtime. This feature is interesting in critical applications that are in continual evolution and that require high availability. The aim of our work is to perform formal verification the correctness of dynamic software updating in Java Card applications by studying the system EmbedDSU. To do so, we first established the correctness of code update. We achieved this by defining formal semantics for update operations on java Card bytecode in order to ensure type safety. Then, we proposed an approach to verify the semantics of updated programs by defining a predicate transformation. Afterward, we were interested in the verification of correction concerning the safe update point detection. We used model checking. This verification allowed us first to fix a deadlock situation in the system and then to establish other correctness properties: activeness safety and updatability. Data update is performed through the application of state transfer functions. For this aspect, we proposed a solution to apply state transfer functions with the preservation of the Java Card virtual machine heap consistency and by allowing a high expressiveness when writing state transfer functions.

Dans cette thèse, nous présentons des approches formelles permettant de simplifier la modélisation et la preuve du calcul distribué. Un système distribué est défini par une collection d’entités de calcul autonomes,qui communiquent ensemble pour accomplir une tâche commune. Chaque entité exécute localement son calcul et ne peut interagir qu’avec ses voisins.Le développement et la preuve du calcul distribué est un défi qui nécessite l’utilisation de méthodes et outils avancés. Dans nos travaux de thèse,nous étudions quelques problèmes fondamentaux du distribués, en utilisant Event-B, et nous proposons des schémas de preuve basés sur une approche“correct-par-construction”. Nous considérons un système distribué défini par réseau fiable, de processus anonymes et avec un modèle de communication basé sur l’échange de messages. Dans certains cas, nous faisons abstraction du modèle de communications en utilisant le modèle des calculs locaux. Nous nous focalisons d’abord sur le problème de détection de terminaison du calcul distribué. Nous proposons un patron formel permettant de transformer des algorithmes “avec détection de terminaison locale” en des algorithmes“avec détection de terminaison globale”. Ensuite, nous explicitons les preuves de correction d’un algorithme d’énumération. Nous proposons un développement formel qui servirait de point de départ aux calculs qui nécessitent l’hypothèse d’identification unique des processus. Enfin, nous étudions le problème du snapshot et du calcul d’état global. Nous proposons une solution basée sur une composition d’algorithmes existants. / In this work, we propose formal approaches for modeling andproving distributed algorithms. Such computations are designed to run oninterconnected autonomous computing entities for achieving a common task :each entity executes asynchronously the same code and interacts locally withits immediate neighbors. Correctness of distributed algorithms is a difficulttask and requires advancing methods and tools. In this thesis, we focus onsome basic problems of distributed computing, and we propose Event-B solutionsbased on the ”correct-by-construction” approach. We consider reliablesystems. We also assume that the network is anonymous and processes communicatewith asynchronous messages. In some cases, we refer to local computationsmodel to provide an abstraction of the distributed computations.We propose a formal framework enhancing the termination detection propertyof distributed algorithms. By relying on refinement and composition,we show that an algorithm specified with “local termination detection”, canbe reused in order to compute the same algorithm with “global terminationdetection”. We then focus on the enumeration problem : we start with anabstract initial specification of the problem, and we enrich it gradually bya progressive and incremental refinement. The computed result constitutesbasic initial steps of others distributed algorithms which assume that processeshave unique identifiers. We therefore focus on snapshot problems, andwe propose to investigate how existing algorithms can be composed, withrefinement, in order to compute a global state in an anonymous network.

Les fonctions de commande et de contrôle sont parmi les plus importantes des systèmes embarqués critiques utilisés dans des activités telles les transports, la santé ou la gestion de l’énergie. Leur impact potentiel sur la sûreté de fonctionnement fait de la vérification de leur correction l’un des points les plus critiques de leur développement. Cette vérification est usuellement effectuée en accord avec les normes de certification décrivant un ensemble d’objectifs à atteindre afin d’assurer un haut niveau de qualité du système et donc de prévenir l’apparition de défauts. Cette vérification du logiciel est traditionnellement basée sur de nombreux tests et des activitiés de relectures de code, toutefois les versions les plus récentes des standards de certification permettent l’utilisation de nouvelles approches de développement telles que l’ingénierie dirigée par les modèles et les méthodes formelles ainsi que l’utilisation d’outil pour assister les processus de développement. Les outils de génération automatique de code sont exploités dans la plupart des processus de développement de systèmes embarqués critiques afin d’éviter des erreurs de programmation liées à l’humain et pour assurer le respect des règles de production de code. Ces outils ayant pour vocation de remplacer les humains pour la production de code, des erreurs dans leur conception peuvent causer l’apparition d’erreurs dans le code généré. Il est donc nécessaire de vérifier que le niveau de qualité de l’outil est le même que celui du code produit en s’assurant que les objectifs spécifiées dans les normes de qualification sont couverts. Nos travaux visent à exploiter l’ingénierie dirigée par les modèles et les méthodes formelles pour développer ces outils et ainsi atteindre un niveau de qualité plus élevé que les approches traditionnelles. Les fonctions critiques de commande et de contrôle sont en grande partie conçues à l’aide de langages graphiques à flot de données. Ces langages sont utilisés pour modéliser des systèmes complexes à l’aide de blocs élémentaires groupés dans des librairies de blocs. Un bloc peut être un objet logiciel sophistiqué exposant une haute variabilité tant structurelle que sémantique. Cette variabilité est à la fois liée aux valeurs des paramètres du bloc ainsi qu’à son contexte d’utilisation. Dans notre travail, nous concentrons notre attention en premier lieu sur la spécification formelle de ces blocs ainsi que sur la vérification de ces spécifications. Nous avons évalué plusieurs approches et techniques dans le but d’assurer une spécification formelle, structurellement cohérente, vérifiable et réutilisable des blocs. Nous avons finalement conçu un langage basé sur l’ingénierie dirigées par les modèles dédié à cette tâche. Ce langage s’inspire des approches des lignes de produit logiciel afin d’assurer une gestion de la variabilité des blocs à la fois correcte et assurant un passage à l’échelle. Nous avons appliqué cette approche et la vérification associée sur quelques exemples choisis de blocs issus d’applications industrielles et l’avons validé sur des prototypes logiciels que nous avons développé. Les blocs sont les principaux éléments des langages d’entrée utilisés pour la génération automatique de logiciels de commande et de contrôle. Nous montrons comment les spécifications formelles de blocs peuvent être transformées en des annotations de code afin de simplifier et d’automatiser la vérification du code généré. Les annotations de code sont vérifiées par la suite à l’aide d’outils spécialisés d’analyse statique de code. En utilisant des observateur synchrones pour exprimer des exigences de haut niveau sur les modèles en entrée du générateur, nous montrons comment la spécification formelle de blocs peut être utilisée pour la génération d’annotations de code et par la suite pour la vérification automatique des exigences. / Control and command softwares play a key role in safety-critical embedded systems used for human related activities such as transportation, healthcare or energy. Their impact on safety makes the assessment of their correctness the central point in their development activities. Such systems verification activities are usually conducted according to normative certification guidelines providing objectives to be reached in order to ensure development process reliability and thus prevent flaws. Verification activities usually relies on tests and proof reading of the software but recent versions of certification guidelines are taking into account the deployment of new development paradigms such as model-based development, and formal methods; or the use of tools in assistance of the development processes. Automatic code generators are used in most safety-critical embedded systems development in order to avoid human related software production errors and to ensure the respect of development quality standards. As these tools are supposed to replace humans in the software code production activities, errors in these tools may result in embedded software flaws. It is thus in turn mandatory to ensure the same level of correctness for the tool itself than for the expected produced code. Tools verification shall be done according to qualification guidelines. We advocate in our work the use of model-based development and formal methods for the development of these tools in order to reach a higher quality level. Critical control and command software are mostly designed using graphical dataflow languages. These languages are used to express complex systems relying on atomic operations embedded in blocks that are gathered in block libraries. Blocks may be sophisticated pieces of software with highly variable structure and semantics. This variability is dependent on the values of the block parameters and of the block's context of use. In our work, we focus on the formal specification and verification of such block based languages. We experimented various techniques in order to ensure a formal, sound, verifiable and usable specification for blocks. We developed a domain specific formal model-based language specifically tailored for the specification of structure and semantics of blocks. This specification language is inspired from software product line concepts in order to ensure a correct and scalable management of the blocks variability. We have applied this specification and verification approach on chosen block examples from common industrial use cases and we have validated it on tool prototypes. Blocks are the core elements of the input language of automatic code generators used for control and command systems development. We show how our blocks formal specification can be translated as code annotations in order to ease and automate the generated code verification. Code annotations are verified using specialised static code analysis tools. Relying on synchronous observers to express high level requirements at the input model level, we show how formal block specification can also be used for the translation of high level requirements as verifiable code annotations discharged using the same specialised tooling. We finally target the assistance of code generation tools qualification activities by arguing on the ability to automatically generate qualification data such as requirements, tests or simulation results for the verification and development of automatic code generators from the formal block specification.

Ce travail porte sur la vérification de composants logiciels dans les systèmes embarqués critiques avioniques. Les conséquences d’une erreur dans de tels systèmes pouvant s'avérer catastrophiques, il se doivent de respecter leur spécification. La vérification formelle tend à prouver cette adéquation si elle est vraie, ou à produire un contre-exemple si elle ne l’est pas. Les méthodes actuelles ne sont pas capable de traiter les les systèmes industriels. La découverte d’informations supplémentaires (invariants) sur le système permet de réduire l’espace de recherche afin de renforcer l’objectif de preuve: les informations découvertes sont suffisantes pour conclure “facilement”. Nous définissons une architecture parallèle permettant à des méthodes de découverte d’invariants de collaborer autour d’un moteur de kinduction. Dans ce contexte nous proposons HullQe, une nouvelle heuristique de génération d’invariants potentiels combinant un calcul de pré-image par élimination de quantificateurs et des calculs d’enveloppes convexes. Nous montrons que HullQe est capable, automatiquement, de renforcer des objectifs de preuve correspondant à la vérification de patrons de conception courants en avionique. Pour autant que nous sachions, les méthodes actuelles sont incapables de conclure sur ces problèmes. Nous détaillons nos améliorations de l’algorithme d’élimination de quantificateurs de Monniaux afin d’assurer le passage à l’échelle sur nos systèmes. Notre framework formel Stuff est une implémentation de notre architecture parallèle composée de HullQe, d'une technique de découverte d’invariants basée sur des templates, et d'une généralisation de PDR à l’arithmétique. / This work studies the verification of software components in avionics critical embedded systems. As the failure of suchsystems can have catastrophic consequences, it is mandatory to make sure they are consistent with their specification.Formal verification consists in proving that a system respects its specification if it does, or to produce a counterexample if itdoes not. Current methods are unable to handle the verification problems stemming from realistic systems. Discoveringadditional information (invariants) on the system can however restrict the search space enough to strengthen the proofobjective: the information discovered allow to "easily" reach a conclusion. We define a parallel architecture for invariantdiscovery methods allowing them to collaborate around a k-induction engine. In this context we propose a new heuristic forthe generation of potential invariants by combining an iterated preimage calculus by quantifier elimination with convexhull computations, called HullQe. We show that HullQe is able to automatically strengthen proof objectives correspondingto safety properties on widespread design patterns in our field. To the best of our knowledge, these systems elude currenttechniques. We also detail our improvements to the quantifier elimination algorithm by David Monniaux in 2008, so that itscales to computing preimages on our systems. Our formal framework Stuff is an implementation of the parallel architecturewe propose in which we implemented not only HullQe, but also a template-based invariant discovery technique, and ageneralisation to Property Directed Reachability to linear real arithmetic and integer octagons.

Lors d’un développement logiciel, et plus particulièrement d’un développement d’applications embarquées avioniques, les activités de vérification représentent un coût élevé. Une des pistes prometteuses pour la réduction de ces coûts est l’utilisation de méthodes formelles. Ces méthodes s’appuient sur des fondements mathématiques et permettent d’effectuer des tâches de vérification à forte valeur ajoutée au cours du développement. Les méthodes formelles sont déjà utilisées dans l’industrie. Cependant, leur difficulté d’appréhension et la nécessité d’expertise pour leur mise en pratique sont un frein à leur utilisation massive. Parallèlement au problème des coûts liés à la vérification logicielle, vient se greffer la complexification des logiciels et du contexte de développement. L’Ingénierie Dirigée par les Modèles (IDM) permet de faire face à ces difficultés en proposant des modèles, ainsi que des activités pour en tirer profit.Le but des travaux présentés dans cette thèse est d’établir un lien entre les méthodes formelles et l’IDM afin de proposer à des utilisateurs non experts une approche de vérification formelle et automatique de programmes susceptible d’améliorer les processus de vérification actuels. Nous proposons de générer automatiquement sur le code source des annotations correspondant aux propriétés comportementales attendues du logiciel, et ce, à partir de son modèle de conception. Ces annotations peuvent ensuite être vérifiées par des outils de preuve déductive, afin de s’assurer que le comportement du code est conforme au modèle. Cette thèse CIFRE s’inscrit dans le cadre industriel d’Atos. Il est donc nécessaire de prendre en compte le contexte technique qui s’y rattache. Ainsi, nous utilisons le standard UML pour la modélisation,le langage C pour l’implémentation et l’outil Frama-C pour la preuve du code. Nous tenons également compte des contraintes du domaine du logiciel avionique dans lequel Atos est impliqué et notamment les contraintes liées à la certification.Les contributions de cette thèse sont la définition d’un sous-ensemble des machines à états UML dédié à la conception comportementale de logiciel avionique et conforme aux pratiques industrielles existantes, la définition d’un patron d’implémentation C, la définition de patrons de génération des propriétés comportementales sur le code à partir du modèle et enfin l’implémentation de l’approche dans un prototype compatible avec l’environnement de travail des utilisateurs potentiels en lien avec Atos. L’approche proposée est finalement évaluée par rapport à l’objectif de départ, par rapport aux attentes de la communauté du génie logiciel et par rapport aux travaux connexes. / During software development, and more specifically embedded avionics applications development, verification is very expensive. A promising lead to reduce its costs is the use of formal methods. Formal methods are mathematical techniques which allow performing rigorous and high-valued verification tasks during software development. They are already applied in industry. However, the high level of expertise required for their use is a major obstacle for their massive use. In addition to the verification costs issue, today software and their development are subject to an increase in complexity. Model Driven Engineering (MDE) allows dealing with these difficulties by offering models, and tasks to capitalize on these models all along the development lifecycle. The goal of this PhD thesis is to establish a link between formal methods and MDE in order to propose to non-expert users a formal and automatic software verification approach which helps to improve software verification processes. We propose to automatically generate annotations, corresponding to the expected behavioural properties of the software, from the design model to the source code. Then, these annotations can be verified using deductive proof tools in order to ensure that the behaviour of the code conforms to the design model. This PhD thesis takes place in the industrial context of Atos. So, it is necessary to take into account its technical specificities. We use UML for the design modeling, the C language for the software implementation and the Frama-C tool for the proof of this implementation. We also take into account the constraints of the avionics field in which Atos intervenes, and specifically the certification constraints. The contributions of this PhD thesis are the definition of a subset of UML state machine dedicated to the behavioural design of embedded avionics software and in line with current industrial practices, the definition of a C implementation pattern, the definition of generation patterns for the behavioural properties from the design model to the source code and the implementation of the whole approach in a prototype in accordance with the working environment of the potential users associated with Atos. The proposed approach is then assessed with respect to the starting goal of the thesis, to the expectation of the software engineering community and to related work.

Les systèmes informatiques sont construits par composition de plusieurs sous-systèmes répartis. La manière dont communiquent ces entités, ou pairs, joue un rôle clé dans la bonne marche du système composé. L'étude détaillée de ces interactions est donc essentielle dans le cadre de la vérification et du développement formel de tels systèmes. Ces interactions se décomposent en deux catégories: la communication synchrone et la communication asynchrone. La communication synchrone admet une transmission instantanée de l'information, le message, entre deux entités. La communication asynchrone, en revanche, prend en compte le découplage de la transmission du message en une opération d'envoi puis de réception avec la possibilité que des événements s'intercalent entre les deux donnant ainsi lieu à des variations de comportement, désirables ou non, des systèmes. Souvent considérée comme une entité monolithique duale du monde synchrone, le monde asynchrone se décline en réalité en de multiples modèles qui peuvent induire sur la communication une grande variété de propriétés qu'il convient de caractériser et comparer. Cette thèse se focalise sur les modèles de communication qui orchestrent l'ordre de délivrance des messages : par exemple les modèles dits FIFO qui assurent que certains messages sont reçus dans l'ordre dans lequel ils ont été émis. Nous considérons des modèles de communication classiques de la littérature ainsi que des variations de ces modèles dont nous explicitons les différences parfois négligées. Dans un premier temps nous proposons une formalisation logique abstraite et homogène des modèles de communication considérés et nous les hiérarchisons en étendant des résultats existants. Nous proposons dans un second temps une approche opérationnelle sous forme d'un outil de vérification de compositions de pairs que nous mécanisons à l'aide du langage de spécification TLA+ et du vérificateur de modèles TLC. Cet outil permet de spécifier des pairs communicants et des propriétés temporelles à vérifier pour les différents modèles de communication de façon modulaire. Pour cela, nous apportons un ensemble de spécifications uniformes et opérationnelles des modèles de communication basé sur la notion d'histoires de messages. Nous identifions et prouvons les conditions de leur conformité aux définitions logiques et validons ainsi la pertinence de notre outil. Dans un troisième temps nous considérons des spécifications concrètes de nos modèles de communication, semblables à nombre de celles présentes dans la littérature. Nous disposons donc d'une hiérarchisation des modèles selon les propriétés d'ordre qu'ils garantissent mais également d'une autre hiérarchisation pour un modèle donné entre sa définition logique abstraite et ses implantations concrètes. Ces deux dimensions correspondent à deux dimensions du raffinement. Nous introduisons graduellement par raffinement la notion de communication asynchrone point à point et prouvons, grâce à la méthode Event-B, tous les liens de raffinement entre les différents modèles de communication et leurs déclinaisons. Nous offrons ainsi une cartographie détaillée des modèles pouvant être utilisée pour en développer de nouveaux ou identifier les modèles les plus adaptés à des besoins donnés. Enfin, nous proposons des pistes d'extension de nos travaux à la communication par diffusion où un message peut être envoyé simultanément à plusieurs destinataires. En particulier, nous montrons les différences induites dans la hiérarchie des modèles et les adaptations à effectuer sur notre outil de vérification pour prendre en compte ce mode de communication / Large computing systems are generally built by connecting several distributed subsystems. The way these entities communicate is crucial to the proper functioning of the overall composed system. An in-depth study of these interactions makes sense in the context of the formal development and verification of such systems. The interactions fall in two categories: synchronous and asynchronous communication. In synchronous communication, the transmission of a piece of information - the message - is instantaneous. Asynchronous communication, on the other hand, splits the transmission in a send operation and a receive operation. This make the interleaving of other events possible and lead to new behaviours that may or may not be desirable. The asynchronous world is often viewed as a monolithic counterpart of the synchronous world. It actually comes in multiple models that provide a wide range of properties that can be studied and compared. This thesis focuses on communication models that order the delivery of messages: for instance, the "FIFO" models ensure that some messages are received in the order of their emission. We consider classic communication models from the literature as well as a few variations. We highlight the differences that are sometimes overlooked. First, we propose an abstract, logical, and homogeneous formalisation of the communication models and we establish a hierarchy that extends existing results. Second, we provide an operational approach with a tool that verifies the compatibility of compositions of peers. We mechanise this tool with the TLA+ specification language and its model checker TLC. The tool is designed in a modular fashion: the commmunicating peers, the temporal compatibility properties, and the communication models are specified independently. We rely on a set of uniform operational specifications of the communication models that are based on the concept of message history. We identify and prove the conditions under which they conform to the logical definitions and thus show the tool is trustworthy. Third, we consider concrete specifications of the communication models that are often found in the literature. Thus, the models are classified in terms of ordering properties and according to the level of abstraction of the different specifications. The concept of refinement covers these two aspects. Thus, we model asynchronous point-to-point communication along several levels of refinement and then, with the Event-B method, we establish and prove all the refinements between the communication models and the alternative specifications of each given model. This work results in a detailed map one can use to develop a new model or find the one that best fits given needs. Eventually we explore ways to extend our work to multicast communication that consists in sending messages to several recipients at once. In particular, we highlight the differences in the hierarchy of the models and how we modify our verification tool to handle this communication paradigm.

Les échanges des informations confidentielles ou critiques dans un environnement public, et donc potentiellement hostile, nécessitent l'emploi de techniques cryptographiques (protocoles et primitives). Malheureusement, l'expérience montre qu'une mauvaise conception, ou une expression peu claire des propriétés et hypothèses de sécurité attendues conduisent à des attaques, et qu'il faut parfois des années avant que celles-ci soient découvertes et corrigées. D'où l'adoption croissante de la sécurité prouvable, où on donne une définition rigoureuse des objectifs de sécurité et des démonstrations mathématiques que ceux-ci sont remplis. Par ailleurs, la complexité et la diversité des systèmes cryptographiques croît également. Il est donc largement admis qu'il n'est plus viable d'écrire ou vérifier manuellement des démonstrations cryptographiques (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005) et qu'il faut développer des méthodes de vérification des systèmes cryptographiques assistées par ordinateur. L'objectif de cette thèse est d'effectuer des progrès significatifs dans cette direction. Plus précisement on s'interesse à la preuve formelle de protocoles cryptographiques. Vérifier des protocoles cryptographiques requiert le développement d'un cadre théorique qui doit permettre: - une modélisation précise des protocoles cryptographiques et des propriétés de sécurité qu'on veut prouver dans le modèle calculatoire. - mise en place de stratégies d'automatisation de preuves. - prise en compte des modèles plus réalistes pour l'adversaire (canaux cachés, ressources de calcul). A la fin de la thèse on a obtenu un cadre formel et un ensemble de méthodes logicielles capable d'aider à la vérification des protocoles cryptographiques. / Critical and private information are exchanged on public environment. To protect it from dishonest users, we use cryptographic tools. Unfortunately, bad conception, poorly written security properties and required security hypothesis lead to attacks, and it may take years before one discover the attack and fix the security schemes involved. In this context, provable security provides formal definitions for security objectives and implied mathematical proofs that these objectives are fullfilled. On another hand, complexity and variety of cryptographic systems are increasing, and proofs by hand are too complicated to write and to verify (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005). Thus, we need computer-assisted verification methods for cryptographic systems. The aim of this thesis is to progress in this direction. More precisely we want significant progress over formal proofs on cryptographic protocols. To verify cryptographic protocols we need to develop a theoritical framework providing: - a precise modelisation for cryptographic protocols and security properties we want to prove in the computationnal model, - designing tactics to automate proofs, - taking into account realistic models for adversary (side-channels...). By the end of the thesis we have enhanced a theoretical framework and computing tools helping verifying cryptographic protocols.