Event B
Résumé
Event B is a modelling language which can describe state-based models and required safety properties. The main objective is to provide a technique for incremental and proof-based development of the reactive systems. It integrates set-theoretical notations and a first-order predicate calculus, models called machines; it includes the concept of refinement expressing the simulation of machine by another one. An Event B machine models a reactive system i.e. a system driven by its environment and to its stimuli. An important property of these machines is that its events preserve the invariant properties defining a set of reachable states. The Evenet B method has been developed from the classical B method and it offers a general framework for developing the correct by construction systems by using an incremental approach for designing the models by refinement. Refinement is a relationship relating two models such that one model is simulating the other one. Refinement is also called refinement and preserves properties of the abstract model in the refined or concrete model. When an abstract model is refined by a concrete model, it means that the concrete model simulates the abstract model and that any safety property of the abstract model is also a safety property of the concrete model. In particular, the concrete model preserves the invariant properties of the abstract model. Event B aims to express models of systems characterized by its invariant and by a list of safety properties. However, we can consider liveness properties as in UNITY or TLA+ but in a restricted way.
La méthode Event B s'appuie sur un langage de modélisation permettant de décrire des modèles à états et les propriétés de sûreté de ces modèles à états. L'objectif principal est de permettre la modélisation incrémentale et prouvée de systèmes réactifs. Elle s'appuie sur un langage intégrant des notations ensemblistes et un calcul des prédicats du premier ordre et offrant la possibilité de définir des modèles de systèmes réactifs, modèles appelés machines; elle y inclut le concept de raffinement qui exprime la simulation d'une machine par une autre machine. Une machine Event B permet de décrire des systèmes réactifs c'est-à-dire des systèmes réagissant à leur environnement et à ses stimuli. Une propriété importante de telles machines est qu'elles maintiennent un invariant qui décrit l'ensemble des états possibles. Le développement de cette méthode a été réalisé à partir de la méthode classique B et propose un cadre général pour développer des systèmes réactifs en utilisant une démarche progressive de conception des modèles par raffinement. Le raffinement est une relation qui lie deux modèles en exprimant un enrichissement d'un modèle par un autre; le raffinement est aussi appelé simulation et le raffinement d'un modèle abstrait par un modèle concret signifie que le modèle concret simule le modèle abstrait et que toutes les propriétés de sûreté du modèle abstrait, en particulier l'invariant abstrait, sont préservées. Event B s'attache à exprimer des modèles de système caractérisés par leur invariant et par des propriétés de sûreté. On peut néanmoins considérer les propriétés de fatalité comme UNITY ou TLA+ mais dans un cadre limité.