The use of formal method techniques can contribute to the production of more reliable and dependable systems. However, a common bottleneck for the industrial adoption of formal methods techniques is proof automation. To address the challenge of proof automation, we aim to improve it by using automated theorem proving techniques. We set one popular formal method technique as our working domain in this thesis, that is, Event-B. More specifically, we target a family of proofs, i.e. invariant preservation (INV) proofs, which can account for a significant part of the proofs that needs human interactions. We apply one of the most successful automated theorem proving techniques, which is rippling, to improve the proof automation of Event-B INV POs. Rippling uses metalevel guidance to automate proofs, and it is in particular useful to develop proof patches to recover proofs based on the meta-level guidance when proof attempts fail. We are especially interested in the case when lemmas are required to recover failed proofs. We combine a scheme-based theory-exploration system, i.e. IsaScheme, with rippling to develop a proof patch for lemma discovery, i.e. ahLemma. In addition to ahLemma, we also develop two proof patches to suggest case-splits and to simplify the goal and hypotheses by rewriting. The combining use of rippling and these proof patches can improve the proof automation of INV POs.

Named data networking (NDN) is a content-centric future Internet architecture that uses routable content names instead of IP addresses to achieve location-independent forwarding. Nevertheless, NDN's design is limited to offering hosted applications a simple content pull mechanism. As a result, increased complexity is needed in developing applications that require more sophisticated content delivery functionalities (e.g., push, publish/subscribe, streaming, generalized forwarding, and dynamic content naming). This thesis introduces a novel Enhanced NDN (ENDN) architecture that offers an extensible catalog of content delivery services (e.g., adaptive forwarding, customized monitoring, and in-network caching control). More precisely, the proposed architecture allows hosted applications to associate their content namespaces with a set of services offered by ENDN. The design of ENDN starts from the current NDN architecture that is gradually modified to meet the evolving needs of novel applications. NDN switches use several forwarding tables in the packet processing pipeline, the most important one being the Forwarding Information Base (FIB). The NDN FIBs face stringent performance requirements, especially in Internet-scale deployments. Hence, to increase the NDN data plane scalability and flexibility, we first propose FCTree, a novel FIB data structure. FCTree is a compressed FIB data structure that significantly reduces the required storage space within the NDN routers while providing fast lookup and modification operations. FCTree also offers additional lookup types that can be used as building blocks to novel network services (e.g., in-network search engine). Second, we design a novel programmable data plane for ENDN using P4, a prominent data plane programming language. Our proposed data plane allows content namespaces to be processed by P4 functions implementing complex stateful forwarding behaviors. We thus extend existing P4 models to overcome their limitations with respect to processing string-based content names. Our proposed data plane also allows running independent P4 functions in isolation, thus enabling P4 code run-time pluggability. We further enhance our proposed data plane by making it protocol-independent using programmable parsers to allow interfacing with IP networks. Finally, we introduce a new control plane architecture that allows the applications to express their network requirements using intents. We employ Event-B machine (EBM) language modeling and tools to represent these intents and their semantics on an abstract model of the network. The resulting EBMs are then gradually refined to represent configurations at the programmable data plane. The Event-B method formally ensures the consistency of the different application requirements using proof obligations and verifies that the requirements of different intents do not contradict each other. Thus, the desired properties of the network or its services, as defined by the intent, are guaranteed to be satisfied by the refined EBM representing the final data-plane configurations. Experimental evaluation results demonstrate the feasibility and efficiency of our proposed architecture.

La sécurité est un élément crucial dans le développement d'un système d'information. On ne peut pas concevoir un système bancaire sans préoccupation sécuritaire. La sensibilité des données d'un système hospitalier nécessite que la sécurité soit la composante majeure d'un tel logiciel. Le contrôle d'accès est un des nombreux aspects de la sécurité. Il permet de définir les conditions de l'exécution d'actions dans un système par un utilisateur. Entre les différentes phases de conception d'une politique de contrôle d'accès et son application effective sur un système déployé, de nombreuses étapes peuvent introduire des erreurs ou des failles non souhaitables. L'utilisation de méthodes formelles est une réponse à ces préoccupations dans le cadre de la modélisation de politiques de contrôle d'accès. L'algèbre de processus EB3 permet une modélisation formelle de systèmes d'information. Son extension EB3SEC a été conçue pour la spécification de politiques de contrôle d'accès. Le langage ASTD, combinaison des statecharts de Harel et des opérateurs de EB3, permet de modéliser graphiquement et formellement un système d'information. Cependant, ces deux méthodes manquent d'outils de vérification et de validation qui permettent de prouver ou de vérifier des propriétés de sécurité indispensables à la validation de politiques de contrôle d'accès. De plus, il est important de pouvoir prouver que l'implémentation d'une politique correspond bien à sa spécification abstraite. Cette thèse définit des règles de traduction de EB3 vers ASTD, d'ASTD vers event-B et vers B. Elle décrit également une architecture formelle exprimée en B d'un filtre de contrôle d'accès pour les systèmes d'information. Cette modélisation en B permet de prouver des propriétés à l'aide du prouveur B ou de vérifier des propriétés avec ProB, un vérificateur de modèles. Enfin, une stratégie de raffinement B pour obtenir une implémentation de ce filtre de contrôle d'accès est présentée. Les raffinements B étant prouvés, l'implémentation correspond donc au modèle initial de la politique de contrôle d'accès / Security is a key aspect in information systems (IS) development. One cannot build a bank IS without security in mind. In medical IS, security is one of the most important features of the software. Access control is one of many security aspects of an IS. It defines permitted or forbidden execution of system's actions by a user. Between the conception of an access control policy and its effective deployment on an IS, several steps can introduce unacceptable errors. Using formal methods may be an answer to reduce errors during the modeling of access control policies. Using the process algebra EB3, one can formally model IS. Its extension, EB3SEC, was created in order to model access control policies. The ASTD notation combines Harel's Statecharts and EB3 operators into a graphical and formal notation that can be used in order to model IS. However, both methods lack tools allowing a designer to prove or verify security properties in order to validate an access control policy. Furthermore, the implementation of an access control policy must correspond to its abstract specification. This thesis defines translation rules from EB3 to ASTD, from ASTD to event-B and from ASTD to B. It also introduces a formal architecture expressed using the B notation in order to enforce a policy over an IS. This modeling of access control policies in B can be used in order to prove properties, thanks to the B prover, but also to verify properties using ProB, a model checker for B. Finally, a refinement strategy for the access control policy into an implementation is proposed. B refinements are proved, this ensures that the implementation corresponds to the initial model of the access control policy

La recherche de la sûreté de fonctionnement des systèmes complexes impose une démarche de conception rigoureuse. Les travaux de cette thèse s’inscrivent dans le cadre la modélisation formelle des systèmes de contrôle autonomes tolérants aux fautes. Le premier objectif a été de proposer une formalisation d’une architecture générique en couches fonctionnelles qui couvre toutes les activités essentielles du système de contrôle et qui intègre des mécanismes de sécurité. Le second objectif a été de fournir une méthode et des outils pour évaluer qualitativement les exigences de sécurité. Le cadre formel de modélisation et d’évaluation repose sur le formalisme Event-B. La modélisation Event-B proposée tire son originalité d’une prise en compte par raffinements successifs des échanges et des relations entre les couches de l’architecture étudiée. Par ailleurs, les exigences de sécurité sont spécifiées à l’aide d’invariants et de théorèmes. Le respect de ces exigences dépend de propriétés intrinsèques au système décrites sous forme d’axiomes. Les preuves que le principe d’architecture proposé satisfait bien les exigences de sécurité attendue ont été réalisées avec les outils de preuve de la plateforme Rodin. L’ensemble des propriétés fonctionnelles et des propriétés relatives aux mécanismes de tolérance aux fautes, ainsi modélisées en Event-B, renforce la pertinence de la modélisation adoptée pour une analyse de sécurité. Cette approche est par la suite mise en œuvre sur un cas d’étude d’un drone ONERA. / The study of complex system safety requires a rigorous design process. The context of this work is the formal modeling of fault tolerant autonomous control systems. The first objective has been to provide a formal specification of a generic layered architecture that covers all the main activities of control system and implement safety mechanisms. The second objective has been to provide tools and a method to qualitatively assess safety requirements. The formal framework of modeling and assessment relies on Event-B formalism. The proposed Event-B modeling is original because it takes into account exchanges and relations betweenarchitecture layers by means of refinement. Safety requirements are first specified with invariants and theorems. The meeting of these requirements depends on intrinsic properties described with axioms. The proofs that the concept of the proposed architecture meets the specified safety requirements were discharged with the proof tools of the Rodin platform. All the functional properties and the properties relating to fault tolerant mechanisms improve the relevance of the adopted Event-B modeling for safety analysis. Then, this approach isimplemented on a study case of ONERA UAV.

As melhores práticas de engenharia de software indicam que a atividade de verificação é fundamental para se alcançar o mínimo de qualidade na construção de um software. Nos processos de desenvolvimento baseados na UML, um dos seus focos principais é detectar inconsistências nos diagramas representativos do software. No entanto, a maioria desses processos, como o Iconix, aplica apenas técnicas informais (ex: inspeções visuais nos modelos), fazendo com que muitas vezes essa atividade seja negligenciada pelos desenvolvedores. Por outro lado, com o avanço das ferramentas automatizadas de verificação, os métodos formais, tais como o Event-B, estão atraindo cada vez mais a atenção das empresas de software. Porém, ainda é difícil convencer os desenvolvedores a adotá-los, pois não estão acostumados com os conceitos matemáticos envolvidos. Assim, este trabalho apresenta uma proposta de inclusão do Event-B no Iconix, dando origem ao BIconix, um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. Mais especificamente, esta tese aborda a tradução automática dos quatro diagramas existentes no Iconix (classes, casos de uso, robustez e sequência) para o Event-B, além de mostrar como esta formalização pode auxiliar na atividade de verificação em pontos específicos e bem definidos no processo proposto. / The best practices of software engineering indicate that the verification activity is essential to achieve some quality during the software construction. In UML-based development processes, one of its main focuses is the detection of inconsistencies in diagrams that represent the software. However, most of these processes, such as Iconix, apply only informal techniques (eg. visual model inspections), often implying the negligence of that activity by developers. Moreover, with the advance of automated verification tools, formal methods, such as Event-B, are increasingly attracting the attention of software companies. However, it is still difficult to convince developers to adopt them, because they are not acquainted with some mathematical concepts. Thus, this paper presents a proposal for the inclusion of Event-B within Iconix, giving rise to BIconix, an object-oriented development process that supports automatic inconsistencies formal verification. More specifically, this thesis addresses the translation of the four existing diagrams in Iconix (classes, use cases, robustness and sequence) to Event- B, and show how this formalization can assist the verification activity in well-defined check points of the proposed process.

Cette thèse vise à définir des techniques pour mieux exploiter les connaissances du domaine dans l’objectif de rendre compte de la réalité de systèmes qualifiés de complexes et critiques. La modélisation est une étape indispensable pour effectuer des vérifications et exprimer des propriétés qu’un système doit satisfaire. La modélisation est une représentation simplificatrice, mais réductionniste de la réalité d’un système. Or, un système complexe ne peut se réduire à un modèle. Un modèle doit s’intégrer dans sa théorie observationnelle pour rendre compte des anomalies qu’il peut y contenir. Notre étude montre clairement que le contexte est la première problématique à traiter car principale source de conflits dans le processus de conception d’un système. L’approche retenue dans cette thèse est celle d’intégrer des connaissances du domaine en associant le système à concevoir à des formalismes déclaratifs qualifiés de descriptifs appelés ontologies. Notre attention est portée au formalisme Event-B dont l’approche correct-par-construction appelée raffinement est le principal mécanisme dans ce formalisme qui permet de faire des preuves sur des représentations abstraites de systèmes pour exprimer/vérifier des propriétés de sûreté et d’invariance. Le premier problème traité concerne la représentation et la modélisation des connaissances du contexte en V&V de modèles. Suite à l’étude des sources de conflits, nous avons établi de nouvelles règles pour une extraction de connaissances liées au contexte par raffinement pour la V&V. Une étude des formalismes de représentation et d’interprétation logiques du contexte a permis de définir un nouveau mécanisme pour mieux structurer les modèles Event-B. Une deuxième étude concerne l’apport des connaissances du domaine pour la V&V. Nous définissons une logique pour le formalisme Event-B avec contraintes du domaine fondées sur les logiques de description, établissons des règles à exploiter pour l’intégration de ces connaissances à des fins de V&V. L’évaluation des propositions faites portent sur des études de cas très complexes telles que les systèmes de vote dont des patrons de conception sont aussi développés dans cette thèse. Nous soulevons des problématiques fondamentales sur la complémentarité que peut avoir l’intégration par raffinement des connaissances du domaine à des modèles en exploitant les raisonnements ontologiques, proposons de définir de nouvelles structures pour une extraction partiellement automatisée / This thesis aims at defining techniques to better exploit the knowledge provided from the domain in order to account for the reality of systems described as complex and critical. Modeling is an essential step in performing verifications and expressing properties that a system must satisfy according to the needs and requirements established in the specifications. Modeling is a representation that simplifies the reality of a system. However, a complex system can not be reduced to a model. A model that represents a system must always fit into its observational theory to account for any anomalies that it may contain. Our study clearly shows that the context is the first issue to deal with as the main source of conflict in the design process of a system. The approach adopted in this thesis is that of integrating knowledge of the domain by associating the system to design with declarative formalisms qualified of descriptive ones that we call ontologies. We pay a particular attention to the Event-B formalism, whose correct-by-construction approach called refinement is the main mechanism at the heart of this formalism, which makes it possible to make proofs on abstract representations of systems for expressing and verifying properties of safety and invariance. The first problem treated is the representation and modeling of contextual knowledge in V&V of models. Following to the study looked at the different sources of conflict, we established new definitions and rules for a refinement context knowledge extraction for Event-B V&V. A study of logical formalisms that represent and interpret the context allowed us to define a new mechanism for better structuring Event-B models. A second study concerns the contribution that domain knowledge can make to the V&V of models. We define a logic for the Event-B formalism with domain constraints based on the description logic, and we define rules to integrate domain knowledge for model V&V. The evaluation of the proposals made deal with very complex case studies such as voting systems whose design patterns are also developed in this thesis. We raise fundamental issues about the complementarity that the integration of domain knowledge can bring to Event-B models by refinement using ontological reasoning, and we propose to define a new structures for a partially automated extraction on both levels, namely the V&V

As melhores práticas de engenharia de software indicam que a atividade de verificação é fundamental para se alcançar o mínimo de qualidade na construção de um software. Nos processos de desenvolvimento baseados na UML, um dos seus focos principais é detectar inconsistências nos diagramas representativos do software. No entanto, a maioria desses processos, como o Iconix, aplica apenas técnicas informais (ex: inspeções visuais nos modelos), fazendo com que muitas vezes essa atividade seja negligenciada pelos desenvolvedores. Por outro lado, com o avanço das ferramentas automatizadas de verificação, os métodos formais, tais como o Event-B, estão atraindo cada vez mais a atenção das empresas de software. Porém, ainda é difícil convencer os desenvolvedores a adotá-los, pois não estão acostumados com os conceitos matemáticos envolvidos. Assim, este trabalho apresenta uma proposta de inclusão do Event-B no Iconix, dando origem ao BIconix, um processo de desenvolvimento orientado a objetos com suporte à verificação formal de inconsistências. Mais especificamente, esta tese aborda a tradução automática dos quatro diagramas existentes no Iconix (classes, casos de uso, robustez e sequência) para o Event-B, além de mostrar como esta formalização pode auxiliar na atividade de verificação em pontos específicos e bem definidos no processo proposto. / The best practices of software engineering indicate that the verification activity is essential to achieve some quality during the software construction. In UML-based development processes, one of its main focuses is the detection of inconsistencies in diagrams that represent the software. However, most of these processes, such as Iconix, apply only informal techniques (eg. visual model inspections), often implying the negligence of that activity by developers. Moreover, with the advance of automated verification tools, formal methods, such as Event-B, are increasingly attracting the attention of software companies. However, it is still difficult to convince developers to adopt them, because they are not acquainted with some mathematical concepts. Thus, this paper presents a proposal for the inclusion of Event-B within Iconix, giving rise to BIconix, an object-oriented development process that supports automatic inconsistencies formal verification. More specifically, this thesis addresses the translation of the four existing diagrams in Iconix (classes, use cases, robustness and sequence) to Event- B, and show how this formalization can assist the verification activity in well-defined check points of the proposed process.

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.

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 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.