Event B

Résumé : 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é.
Type de document :
Chapitre d'ouvrage
Jean-Louis Boulanger. Mise en oeuvre de la méthode B, HERMES, 2013, Informatique et Systèmes d'Informations, ISBN : 978-2-7462-3810-7
Liste complète des métadonnées

https://hal.inria.fr/hal-00926335
Contributeur : Dominique Méry <>
Soumis le : jeudi 9 janvier 2014 - 14:35:45
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24

Identifiants

  • HAL Id : hal-00926335, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Event B. Jean-Louis Boulanger. Mise en oeuvre de la méthode B, HERMES, 2013, Informatique et Systèmes d'Informations, ISBN : 978-2-7462-3810-7. 〈hal-00926335〉

Partager

Métriques

Consultations de la notice

427