Le thème principal de cette recherche est d'étudier et développer des techniques pour la modélisation des systèmes où la sécurité est critique. Cette thèse est focalisé sur l'étape de la spécification du domaine où de tels systèmes vont fonctionner, et de sa validation. La contribution de cette thèse est double. D'abord, nous modélisons le domaine des transports terrestres, un bon candidat pour cette étude en raison de sa nature critique vis-à-vis de la sécurité, dans le cadre formel de B événementiel et proposent quelques directives pour cette activité. Ensuite, nous présentons une approche, basée sur les techniques de l'animation et des transformations, pour la validation par étapes des spécifications formelles.

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 / This thesis aims at the specification, verification and validation of safety-critical systems with formal methods, in particular, with Event-B. We assessed the usability of Event-B by the development of platooning control algorithms, specially how it scaled up from a simplified 1D version to a more realistic 2D version. The critical analysis of the 1D platooning model uncovered some anomalous behaviors. The difficulty of expressing the deadlock-freeness theorems in Event-B motivated us to develop a tool, the generator of deadlock-freeness theorems, to automatically construct these theorems. Our assessment confirmed that the mathematical proofs are not sufficient to assure the correctness of a formal specification: a formal specification should also be validated. We believe that the validation activities, like the verification activities, should be associated with each refinement during the development. To do that, we need better validation tools. The state-of-the-art tools which can execute Event-B models failed in highly non-deterministic models. Therefore we designed and implemented a new execution tool, JeB, which is a JavaScript simulation framework for Event-B. JeB allows users to safely insert hand-coded pieces of code to supply deterministic computations where the automatic translation fails. To achieve this goal, we have defined a set of proof-obligations which, when discharged, guarantee the correctness of the simulations with respect to the model.

Le travail de thèse présente une méthode de développement de systèmes automatisés basée sur les méthodes formelles B et TLA+. Le développement par raffinement est au cœur de la méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé par le dispositif physique et son environnement et un contrôleur pilotant ce dernier. Il est exprimé par un produit synchronisé sur les actions de ces deux composants. La première contribution de la thèse concerne la proposition d'une approche qui combine le B événementiel et le langage de modélisation TLA+ pour la vérification des propriétés de vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant d'exprimer des propriétés de vivacité. Nous développons un prototype pour la transformation d'un modèle B en un module TLA+ sur lequel nous effectuons la preuve des propriétés de vivacité avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis, nous proposons l'utilisation des diagrammes de prédicats qui sont des abstractions des systèmes modélisés en TLA+. La deuxième contribution est la proposition d'une technique pour représenter explicitement le temps en B événementiel. Cette technique s'appuie sur la réalisation d'un entrelacement entre un processus qui gère le temps avec les autres processus du système. Le temps modélisé est discret et son écoulement est modélisé par des événements. Cette approche est assez différente des systèmes temporisés où l'on considère que le temps s'écoule indépendamment du système. Dans la troisième contribution, nous proposons une approche de développement des systèmes automatisés en utilisant la technique de composition où il s'agit de développer conjointement le contrôleur et le composant physique qu'il contrôle et appliquer le raffinement aussi bien sur le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction porte sur le comportement du système automatisé qui résulte de la composition du contrôleur et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits. La dernière contribution porte sur la définition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des systèmes de production manufacturière. Ce type de patron prouvé permet d'utiliser l'abstraction discrète de l'effet d'un processus continu agissant pendant un certain temps / This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while

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.