En informatique, la notion de ressource est une notion centrale. Nous considérons comme ressource toute entité pouvant être composée ou décomposée en sous-entités. Plusieurs logiques ont été proposées afin de modéliser et d’exprimer des propriétés sur celles-ci, comme la logique BI exprimant des propriétés de partage et de séparation. Puisque les systèmes informatiques manipulent des ressources, la proposition de nouveaux modèles capturant la dynamique de ces ressources, ainsi que la vérification et la preuve de propriétés sur ces modèles, sont des enjeux cruciaux. Dans ce contexte, nous définissons de nouvelles logiques permettant la modélisation logique de la dynamique des ressources, proposant de nouveaux modèles et permettant l’expression de nouvelles propriétés sur cette dynamique. De plus, pour ces logiques, nous proposons des méthodes des tableaux et d’extraction de contre-modèles. Dans un premier temps, nous définissons de nouveaux réseaux de Petri, nommés ß-PN, et proposons une nouvelle sémantique à base de ß-PN pour BI. Puis nous proposons une première extension modale de BI, nommée DBI, permettant la modélisation de ressources ayant des propriétés dynamiques, c’est-à-dire évoluant en fonction de l’état courant d’un système. Ensuite, nous proposons une logique, nommée DMBI, modélisant des systèmes manipulant/produisant/consommant des ressources. Par ailleurs, nous proposons une nouvelle logique (LSM) possédant de nouvelles modalités multiplicatives (en lien avec les ressources). Pour finir, nous introduisons la séparation au sein des logiques épistémiques, obtenant ainsi une nouvelle logique ESL, exprimant de nouvelles propriétés épistémiques / In computer science, the notion of resource is a central concern. We consider as a resource, any entity that can be composed or decomposed into sub-entities. Many logics were proposed to model and express properties on these resources, like BI logic, a logic about sharing and separation of resources. As the computer systems manipulate resources, a crucial issue consists in providing new models that capture the dynamics of resources, and also in verifying and proving properties on these models. In this context, we define new logics with new models and new languages allowing to respectively capture and express new properties on the dynamics of resources. Moreover, for all these logics, we also study the foundations of proof search and provide tableau methods and counter-model extraction methods. After defining new Petri nets, called ß-PN, we propose a new semantics based on ß-PN for BI logic, that allows us to show that BI is able to capture a kind of dynamics of resources. After observing that it is necessary to introduce new modalities in BI logic, we study successively different modal extensions of BI. We define a logic, called DBI, that allows us to model resources having dynamic properties, meaning that they evolve during the iterations of a system. Then, we define a logic, called DMBI, that allows us to model systems that manipulate/produce/consume resources. Moreover, we define a new modal logic, called LSM, having new multiplicative modalities, that deals with resources. Finally, we introduce the notion of separation in Epistemic Logic, obtaining a new logic, called ESL, that models and expresses new properties on agent knowledge

Les “smart-devices” tels les smartphones, tablettes et même les montres ont été largement démocratisés au cours de la dernière décennie. Dans nos sociétés occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arrière de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limités, en termes d’utilisation, à de la simple communication par SMS ou bien téléphone, on se fie à eux pour stocker nos photos et données personnelles, ces dernières parfois aussi critiques que des données de paiement bancaires, on gère nos contacts et finances, se connecte à notre boite mail ou un site marchand depuis eux. . . Des exemples récents nous fournissent d’ailleurs un aperçu des tâches de plus en plus complexes que l’on confie à ces outils : l’Estonie autorise l’utilisation de smartphones pour participer aux scrutins nationaux et en 2017, la société Transport for London a lancé sa propre application autorisant l’émulation d’une Oyster card et son rechargement pour emprunter son réseau de transports publics. Plus les services se complexifient, plus la confiance qui leur est accordée par les groupes industriels et les utilisateurs grandit. Nous nous intéressons ici aux protocoles cryptographiques qui définissent les échanges entre les outils et entités qui interviennent dans l’utilisation de tels services et aux garanties qu’ils proposent en termes de sécurité (authentification mutuelle des agent, intégrité des messages circulant, secret d’une valeur critique…). Moult exemples de la littérature et de la vie courante ont démontré que leur élaboration était hautement vulnérable à des erreurs de design. Heureusement, des années de recherches nous ont fournis des outils pour rendre cette tâche plus fiable, les méthodes formelles font partie de ceux-là. Il est possible de modeler un protocole cryptographique comme un processus abstrait qui manipule des données et primitives cryptographiques elles aussi modélisées comme des termes et fonctions abstraites. On met le protocole à l’épreuve face à un attaquant actif et on peut spécifier mathématiquement les propriétés de sécurité qu’il est censé garantir. Ces preuves de sécurité peuvent être automatisées grâce à des outils tels que ProVerif ou bien Tamarin. L’une des grandes difficultés lorsque l’on cherche à concevoir et prouver formellement la sécurité d’un protocole de niveau industriel réside dans le fait que ce genre de protocole est généralement très long et doit satisfaire des propriétés de sécurité plus complexes que certains protocoles universitaires. Au cours de cette thèse, nous avons souhaité étudier deux cas d’usage : le vote électronique et le paiement mobile. Dans les deux cas, nous avons conçu et prouvé la sécurité d’un protocole répondant aux problématiques spécifiques à chacun des cas d’usage. Dans le cadre du vote électronique, nous proposons le protocole Belenios VS, une variante de Belenios RF. Nous définissons l’écosystème dans lequel le protocole est exécuté et prouvons sa sécurité grâce à ProVerif. Belenios VS garantit la confidentialité du vote et le fait qu’un utilisateur puisse vérifier que son vote a bien fait parti du résultat final de l’élection, tout cela même si l’outil utilisé par le votant est sous le contrôle d’un attaquant. Dans le cadre du paiement, nous avons proposé la première spécification ouverte de bout en bout d’une application de paiement mobile. Sa conception a pris en compte le fait qu’elle devait pouvoir s’adapter à l’écosystème de paiement déjà existant pour être largement déployable et que les coûts de gestion, de développement et de maintenance de la sécurité devait être optimisés / The last decade has seen the massive democratization of smart devices such as phones, tablets, even watches. In the wealthiest societies of the world, not only do people have their personal computer at home, they now carry one in their pocket or around their wrist on a day to day basis. And those devices are no more used simply for communication through messaging or phone calls, they are now used to store personal photos or critical payment data, manage contacts and finances, connect to an e-mail box or a merchant website... Recent examples call for more complex tasks we ask to such devices: Estonia voting policy allows the use of smart ID cards and smartphones to participate to national elections. In 2017, Transport for London launched the TfL Oyster app to allow tube users to top up and manage their Oyster card from their smartphone. As services grow with more complexity, so do the trust users and businesses put in them. We focus our interest into cryptographic protocols which define the exchanges between devices and entities so that such interaction ensure some security guarantees such as authentication, integrity of messages, secrecy… Their design is known to be an error prone task. Thankfully, years of research gave us some tools to improve the design of security protocols, among them are the formal methods: we can model a cryptographic protocol as an abstract process that manipulates data and cryptographic function, also modeled as abstract terms and functions. The protocol is tested against an active adversary and the guarantees we would like a protocol to satisfy are modeled as security properties. The security of the protocol can then be mathematically proven. Such proofs can be automated with tools like ProVerif or Tamarin. One of the big challenge when it comes to designing and formally proving the security an “industrial- level” protocol lies in the fact that such protocols are usually heavier than academic protocols and that they aim at more complex security properties than the classical ones. With this thesis, we wanted to focus on two use cases: electronic voting and mobile payment. We designed two protocols, one for each respective use case and proved their security using automated prover tools. The first one, Belenios VS, is a variant of an existing voting scheme, Belenios RF. It specifies a voting ecosystem allowing a user to cast a ballot from a voting sheet by flashing a code. The protocol’s security has been proven using the ProVerif tool. It guarantees that the vote confidentiality cannot be broken and that the user is capable of verifying their vote is part of the final result by performing a simple task that requires no technical skills all of this even if the user’s device is compromised – by a malware for instance. The second protocol is a payment one that has been conceived in order to be fully scalable with the existing payment ecosystem while improving the security management and cost on the smartphone. Its security has been proven using the Tamarin prover and holds even if the user’s device is under an attacker’s control

L’analyse de codes malveillants est un domaine de recherche en pleine expansion de par la criticité des infrastructures touchées et les coûts impliqués de plus en plus élevés. Ces logiciels utilisent fréquemment différentes techniques d’évasion visant à limiter la détection et ralentir les analyses. Parmi celles-ci, l’obfuscation permet de cacher le comportement réel d’un programme. Cette thèse étudie l’utilité de l’Exécution Symbolique Dynamique (DSE) pour la rétro-ingénierie. Tout d’abord, nous proposons deux variantes du DSE plus adaptées aux codes protégés. La première est une redéfinition générique de la phase de calcul de prédicat de chemin basée sur une manipulation flexible des concrétisations et symbolisations tandis que la deuxième se base sur un algorithme d’exécution symbolique arrière borné. Ensuite, nous proposons différentes combinaisons avec d’autres techniques d’analyse statique afin de tirer le meilleur profit de ces algorithmes. Enfin tous ces algorithmes ont été implémentés dans différents outils, Binsec/se, Pinsec et Idasec, puis testés sur différents codes malveillants et packers. Ils ont permis de détecter et contourner avec succès les obfuscations ciblées dans des cas d’utilisations réels tel que X-Tunnel du groupe APT28/Sednit. / Malware analysis is a growing research field due to the criticity and variety of assets targeted as well as the increasing implied costs. These softwares frequently use evasion tricks aiming at hindering detection and analysis techniques. Among these, obfuscation intent to hide the program behavior. This thesis studies the potential of Dynamic Symbolic Execution (DSE) for reverse-engineering. First, we propose two variants of DSE algorithms adapted and designed to fit on protected codes. The first is a flexible definition of the DSE path predicate computation based on concretization and symbolization. The second is based on the definition of a backward-bounded symbolic execution algorithm. Then, we show how to combine these techniques with static analysis in order to get the best of them. Finally, these algorithms have been implemented in different tools Binsec/se, Pinsec and Idasec interacting alltogether and tested on several malicious codes and commercial packers. Especially, they have been successfully used to circumvent and remove the obfuscation targeted in real-world malwares like X-Tunnel from the famous APT28/Sednit group.

Dans des système concurrent, potentiellement embarqués et distribué, il est souvent crucial d'être capable de déterminer quel(s) composant(s) est(sont) responsable(s) d'une défaillance, que ce soit pour debbuger, établir une responsabilité contractuelle du fournisseur des composant, ou pour isolée, ou redémarrer les composants défaillants. Le diagnostic s'appuie sur l'analyse de la causalité logique pour distinguer les composants ayant contribué à la défaillance du système, de ceux ayant eu peu ou pas d'impact sur cette dernière. Plus précisément, un composant C est une cause nécessaire, si la propriété P du système n'aurait pas été violée si C s'était comporté selon sa spécification S. De même, C est une cause suffisante de la violation de P (défaillance du système) si P aurait été violée, même si tous les composants, sauf C, avait respecté leur spécification. Autrement dit, la violation de S, du composant C, est suffisante pour violer P. L'approche a été formalisée, initialement, pour des modèle d'interaction BIP. Le but de ce projet est de formaliser un raisonnement similaire pour des programmes fonctionnels, où les fonctions sont équipées d'invariant décrivant leur comportement attendu. L'analyse prendrait en entrée une trace d'exécution (défaillante) et les invariant, et déterminerait quelle(s) fonction(s) est(sont) une(des) cause(s) de la défaillance. L'approche devra être implémenté et appliquée à des cas d'études provenant du domaine médical, ou de l'automatique. / In a concurrent, possibly embedded and distributed system, it is often crucial to be able to determine which component(s) caused an observed failure - be it for debugging, to establish the contractual liability of component providers, or to isolate or reset the failing component. The diagnostic relies on analysis of logical causality to distinguish component failures that actually contributed to the outcome from failures that had little or no impact on the system-level failure . More precisely, necessary causality of a component C characterizes cases when a system-level property P would not have been violated if the specification S of C had been fulfilled. Sufficient causality characterizes cases where P would have been violated even if all the components but C had fulfilled their specifications. In other words, the violation of S by C was sufficient to violate P. The initial approach to causality analysis on execution traces was formalized for the BIP interaction model. The goal of this project is to formalize a similar reasoning for functional programs where functions are equipped with invariants describing the expected behavior. The analysis should take a (faulty) execution trace and the invariants and determine which function(s) caused the failure. The results should be implemented and applied to case studies from the medical and automotive domains.

Cette thèse se situe au croisement de deux domaines : la sûreté de fonctionnement des systèmes critiques et les méthodes formelles. Nous cherchons à établir la cohérence des analyses de sûreté de fonctionnement réalisées à l’aide de modèles représentant un même système à des niveaux de détail différents. Pour cela, nous proposons une notion de raffinement dans le cadre de la conception de modèles AltaRica : un modèle détaillé raffine un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vérification du raffinement de modèles AltaRica est supportée par l’outil de model-checking MecV. Ceci permet de réaliser des analyses multi-systèmes à l’aide de modèles à des niveaux de détail hétérogènes : le système au centre de l’étude est détaillé tandis que les systèmes en interface sont abstraits. Cette approche a été appliquée à l’étude d’un système de contrôle de gouverne de direction d’un avion connecté à un système de génération et distribution électrique. / This thesis links two fields : system safety analyses and formal methods.We aim at checking the consistensy of safety analyses based on formal models that represent a system at different levels of detail. To reach this objective, we introduce a refinement notion in the AltaRica modelling process : a detailed model refines an abstract model if the abstract model simulates the detailed model. The AltaRica model refinement verification is supported by the MecV model-checker. This allows to perform multi-system safety analyses using models with heterogeneous levels of detail : the main system is detailed whereas the interfaced systems remain abstract. This approach has been applied to the analysis of a rudder control system linked to an electrical power generation and distribution system.

Le Cloud Computing est de plus en plus utilisé pour le déploiement et l'exécution des applications métiers et plus particulièrement des applications à base de services (AbSs). L'élasticité à différents niveaux est l'une des propriétés fournies par le Cloud. Son principe est de garantir la fourniture des ressources nécessaires et suffisantes pour la continuité de l'exécution optimale des services Cloud. La fourniture des ressources doit considérer la variation de la demande pour éviter la sous-utilisation et la surutilisation de ces dernières. Il est évident que la fourniture d'infrastructures et/ou de plateformes élastiques n'est pas suffisante pour assurer l'élasticité des applications métiers déployées. En effet, il est aussi nécessaire de considérer l'élasticité au niveau des applications. Ceci permet l'adaptation dynamique des applications déployées selon la variation des demandes. Par conséquent, les applications métiers doivent être fournies avec des mécanismes d'élasticité permettant leur adaptation tout en assurant les propriétés fonctionnelles et non-fonctionnelles désirées. Dans nos travaux, nous nous sommes intéressés à la fourniture d'une approche holistique pour la modélisation, l'évaluation et la mise en oeuvre des mécanismes d'élasticité des AbSs dans le Cloud. En premier lieu, nous avons proposé un modèle formel pour l'élasticité des AbSs. Pour cela, nous avons modélisé les AbSs en utilisant les réseaux de Petri et défini deux opérations d'élasticité (la duplication et la consolidation). En outre, nous avons proposé de coupler ces deux opérations avec un contrôleur d'élasticité. Pour assurer l'élasticité des AbSs, le contrôleur analyse l'exécution des AbSs et prend des décisions sur les opérations d'élasticité (duplication/consolidation). Après la définition de notre modèle pour l'élasticité des AbSs, nous nous sommes intéressés à l'évaluation de l'élasticité avant de l'implémenter dans des environnements Cloud réels. Pour cela, nous avons proposé d'utiliser notre contrôleur d'élasticité comme un Framework pour la validation et l'évaluation de l'élasticité en utilisant des techniques de vérification et de simulation. Enfin, nous avons mis en oeuvre l'élasticité des AbSs dans des environnements Cloud réels. Pour cela, nous avons proposé deux approches. La première approche encapsule les AbSs non-élastiques dans des micro-conteneurs, étendus avec nos mécanismes d'élasticité, avant de les déployer sur des infrastructures Cloud. La seconde approche intègre notre contrôleur d'élasticité dans une infrastructure autonomique afin de permettre l'ajout dynamique des fonctionnalités d'élasticité aux AbSs déployées sur des plateformes Cloud / Cloud computing is being increasingly used for deploying and executing business processes and particularly Service-based Business Processes (SBPs). Among other properties, Cloud environments provide elasticity at different scopes. The principle of elasticity is to ensure the provisioning of necessary and sufficient resources such that a Cloud service continues running smoothly even when the number or quantity of its utilization scales up or down, thereby avoiding under-utilization and over-utilization of resources. It is obvious that provisioning of elastic infrastructures and/or platforms is not sufficient to provide elasticity of deployed business processes. In fact, it is also necessary to consider the elasticity at the application scope. This allows the adaptation of deployed applications during their execution according to demands variation. Therefore, business processes should be provided with elasticity mechanisms allowing their adaptation to the workload changes while ensuring the desired functional and non-functional properties. In our work, we were interested in providing a holistic approach for modeling, evaluating and provisioning of elastic SBPs in the Cloud. We started by proposing a formal model for SBPs elasticity. To do this, we modeled SBPs using Petri nets and defined two elasticity operations (duplication / consolidation). In addition, we proposed to intertwine these elasticity operations with an elasticity controller that monitors SBPs execution, analyzes monitoring information and executes the appropriate elasticity operation (duplication/consolidation) in order to enforce the elasticity of SBPs. After facing the challenge of defining a model and mechanisms for SBPs elasticity, we were interested in the evaluation of elasticity before implementing it in real environments. To this end, we proposed to use our elasticity controller as a framework for the validation and evaluation of elasticity using verification and simulation techniques. Finally, we were interested in the provisioning of elasticity mechanisms for SBPs in real Cloud environments. For this aim, we proposed two approaches. The first approach packages non-elastic SBPs in micro-containers, extended with our elasticity mechanisms, before deploying them in Cloud infrastructures. The second approach integrates our elasticity controller in an autonomic infrastructure to dynamically add elasticity facilities to SBPs deployed on Cloud platforms

Ce mémoire présente plusieurs définitions de sémantiques formelles et de transformations de programmes, et expose les choix de conception associés. En particulier, ce mémoire décrit une transformation de programmes inspirée de l'évaluation partielle et dédiée à la compréhension de programmes scientifiques écrits en Fortran. Il détaille également le front-end d'un compilateur réaliste du langage C, ayant été formellement vérifié en C.

Nous étudions la modélisation et la validation hors-ligne des applications temps-réel en environnement monoprocesseur, qui prend explicitement en compte l'échange des messages, le partage des ressources et les instructions conditionnelles entre les tâches. Notre objectif est de mettre en évidence l'impact de ces paramètres sur l'analyse des applications. Classiquement, ces applications sont modélisées de façon linéaire, en encapsulant les blocs conditionnels, et les séquences sont utilisées pour leur validation. Nous proposons une approche de modélisation et de validation arborescente, qui permet de considérer de façon explicite les blocs conditionnels, et qui utilise les arbres d'ordonnancement pour la validation. Nous comparons ensuite ces deux approches, et prouvons que les premières sont parfois trop pessimistes, c'est à dire qu'elles peuvent conduire à déclarer certaines applications comme non ordonnançables, alors qu'en réalité elles le sont. Nous commençons par construire un générateur d'arbres d'ordonnancement valides. La complexité du générateur étant exponentielle en fonction du nombre de tâches, cette approche est di cile à mettre en ÷uvre dans la pratique. Nous proposons donc une approche de modélisation bas ée sur les réseaux de Petri. Ce réseau sera utilisé pour générer les arbres valides, par construction du graphe de marquages, et la complexité pourra être réduite grâce à des heuristiques.

Les systèmes multi-agents (SMA) peuvent être utilisé pour modéliser les phénomènes qui peuvent être décomposés en plusieurs agents qui interagissent et qui existent au sein d'un environnement. En particulier, ils peuvent être utilisés pour modéliser les sociétés humaines et animales, aux fins de l'analyse de leurs propriétés par des moyens de calcul. Cette thèse est consacrée à l'analyse automatisée d'un type particulier de ces modèles sociaux, à savoir, celles qui sont fondées sur les principes comportementalistes, qui contrastent avec les approches cognitives plus dominante dans la littérature des SMAs. La caractéristique des théories comportementalistes est l'accent mis sur la définition des comportements basée sur l'interaction entre les agents et leur environnement. De cette manière, non seulement des actions réflexives, mais aussi d'apprentissage, les motivations, et les émotions peuvent être définies. Plus précisément, dans cette thèse, nous introduisons une architecture formelle d'agent (spécifiée avec la Notation Z) basée sur la théorie d'analyse comportementale de B. F. Skinner, ainsi que une notion appropriée et formelle de l'environnement (basée sur l'algèbre de processus pi-calculus) pour mettre ces agents ensemble dans un SMA. La simulation est souvent utilisée pour analyser les SMAs. Les techniques consistent généralement à simuler le SMA plusieurs fois, soit pour recueillir des statistiques, soit pour voir ce qui se passe à travers l'animation. Toutefois, les simulations peuvent être utilisés d'une manière plus orientée vers la vérification si on considère qu'elles sont en réalité des explorations de grandes espaces d'états. Dans cette thèse nous proposons une technique de vérification nouvelle basé sur cette idée, qui consiste à simuler un SMA de manière guidée, afin de vérifier si quelques hypothèses sur lui sont confirmées ou non. À cette fin, nous tirons profit de la position privilégiée que les environnements sont dans les SMAs de cette thèse: la spécification formelle de l'environnement d'un SMA sert à calculer les évolutions possibles du SMA comme un système de transition, établissant ainsi l'espace d'états à vérifier. Dans ce calcul, les agents sont pris en compte en les simulant afin de déterminer, à chaque état de l'environnement, quelles sont leurs actions. Chaque exécution de la simulation est une séquence d'états dans cet espace d'états, qui est calculée à la volée, au fur et à mesure que la simulation progresse. L'hypothèse à étudier, à son tour, est donnée comme un autre système de transition, appelé objectif de simulation, qui définit les simulations désirables et indésirables (e.g., "chaque fois que l'agent fait X, il fera Y plus tard"). Il est alors possible de vérifier si le SMA est conforme à l'objectif de simulation selon un certain nombre de notions de satisfiabilité très précises. Algorithmiquement, cela correspond à la construction d'un produit synchrone de ces deux systèmes de transitions (i.e., celui du SMA et l'objectif de simulation) à la volée et à l'utiliser pour faire fonctionner un simulateur. C'est-à-dire, l'objectif de simulation est utilisé pour guider le simulateur, de sorte que seuls les états concernés sont en réalité simulés. À la fin d'un tel algorithme, il délivre un verdict concluant ou non concluant. Si c'est concluant, il est connu que le SMA est conforme à l'objectif de simulation par rapport aux observations qui ont été faites lors des simulations. Si c'est non-concluant, il est possible d'effectuer quelques ajustements et essayer à nouveau. En résumé, donc, dans cette thèse nous fournissons quatre nouveaux éléments: (i) une architecture d'agent; (ii) une spécification formelle de l'environnement de ces agents, afin qu'ils puissent être composés comme un SMA; (iii) une structure pour décrire les propriétés d'intérêt, que nous avons nommée objectif de simulation, et (iv) une technique pour l'analyse formelle du SMA résultant par rapport à un objectif de simulation. Ces éléments sont mis en œuvre dans un outil, appelé Simulateur Formellement Guidé (FGS, de l'anglais Formally Guided Simulator). Des études de cas exécutables dans FGS sont fournies pour illustrer l'approche.

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit