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

Un des défis majeurs pour le développement des Systèmes Multi-Agents (SMA) auto-organisateurs est de garantir la convergence du système vers la fonction globale attendue par un observateur externe et de garantir que les agents sont capables de s'adapter face aux perturbations. Dans la littérature, plusieurs travaux se sont basés sur la simulation et le model-checking pour analyser les SMA auto-organisateurs. La simulation permet aux concepteurs d'expérimenter plusieurs paramètres et de créer certaines heuristiques pour faciliter la conception du système. Le model-checking fournit un support pour découvrir les blocages et les violations de propriétés. Cependant, pour faire face à la complexité de la conception des SMA auto-organisateurs, le concepteur a également besoin de techniques qui prennent en charge non seulement la vérification, mais aussi le processus de développement lui-même. En outre, ces techniques doivent permettre un développement méthodique et faciliter le raisonnement sur divers aspects du comportement du système à différents niveaux d'abstraction. Dans cette thèse, trois contributions essentielles ont été apportées dans le cadre du développement et la vérification formelle des SMA auto-organisateurs: une formalisation à l'aide du langage B-événementiel des concepts clés de ces systèmes en trois niveaux d'abstraction (micro, méso et macro), une expérimentation d'une stratégie de raffinement descendante pour le développement des SMA auto-organisateurs et la proposition d'un processus de raffinement ascendant basé sur des patrons de raffinement. / A major challenge for the development of self-organizing MAS is to guarantee the convergence of the system to the overall function expected by an external observer and to ensure that agents are able to adapt to changes. In the literature, several works were based on simulation and model-checking to study self-organizing MAS. The simulation allows designers to experiment various settings and create some heuristics to facilitate the system design. Model checking provides support to discover deadlocks and properties violations. However, to cope with the complexity of self-organizing MAS, the designer also needs techniques that support not only verification, but also the development process itself. Moreover, such techniques should support disciplined development and facilitate reasoning about various aspects of the system behavior at different levels of abstraction. In this thesis, three essential contributions were made in the field of formal development and verification of self-organizing MAS: a formalization with the Event-B language of self-organizing MAS key concepts into three levels of abstraction, an experimentation of a top-down refinement strategy for the development of self-organizing MAS and the definition of a bottom-up refinement process based on refinement patterns.

L’objet de ce travail doctoral est d’analyser les conditions d’émergence d’une démarche de changement RSE et de diffusion de connaissances entre les parties prenantes d’un événementiel dans le contexte spécifique d’un centre des congrès et/ou d’un parc des expositions. En combinant la théorie des parties prenantes, la théorie de l’acteur réseau et les conceptualisations théoriques du transfert de connaissances, notre recherche propose d’appréhender simultanément la manière dont chaque partie prenante va être actrice de la dynamique de changement RSE d’un événement ainsi que les mécanismes de construction et de diffusion des connaissances RSE entre ces dernières durant ce processus. Notre méthodologie empirique est basée sur une étude de cas unique enchâssée réalisée dans le cadre d’une convention CIFRE au sein d’Angers Expo Congrès, une entreprise en charge de la gestion d’un centre des congrès et d’un parc des expositions. Dans cette optique, nous avons étudié deux unités d’analyse : 1) la démarche RSE de l’organisation et 2) celle de son salon professionnel Sival. Les résultats de notre recherche permettent d’identifier et de positionner les parties prenantes dans la dynamique de changement RSE d’un événement. Ils mettent aussi en lumière les modalités de l’action collective autour de la dynamique de changement RSE d’un événement et révèlent les modalités de transfert inter-organisationnel de connaissances entre ses parties prenantes. Ce travail doctoral propose conjointement une véritable méthodologie de conduite du changement RSE associant les parties prenantes d’un événementiel et des leviers d’actions pour faciliter la diffusion des connaissances RSE entre elles. / The purpose of this doctoral research is to analyse the conditions for the emergence of a CSR change process and knowledge transfer between an event stakeholders in the specific context of a convention centre and/or exhibition complex. By combining stakeholder theory, actor network theory and theoretical conceptualizations of knowledge transfer approach, our research proposes simultaneously to understand how each stakeholder is an actor in the event CSR process and the methods facilitating the construction and dissemination of CSRknowledge between them during the process. Our empirical methodology is based on a single case study carried out under a research contract (CIFRE) in Angers Expo Congrès, a company in charge of a convention centre and exhibition complex. In this context, we study two units of analysis: 1) the CSR approach of the organization and 2) the CSR approach of the tradeshow Sival. The results of our research identify and positionthe stakeholders in the event CSR change process. They also highlight the methods of collective action around the event CSR change process and the methods of inter-organizational knowledge transfer between stakeholders. This doctoral research jointly offers a real methodology for conducting CSR change involving event stakeholders and levers for action in order to facilitate the dissemination of CSR knowledge between them.