3.2.3 La méthode Event-B
Event-B [4] est une méthode basée sur la
méthode B avec un aspect événementiel. Elle permet de
spécifier le comportement d'un système appelé «
système d'événements » de manière à
inclure ses propriétés critiques dans la conception. Dans la
méthode Event-B, le modèle initial est successivement
raffiné plusieurs fois pour atteindre une modélisation correcte
par construction [3]. Les propriétés introduites sont
également prouvées et l'utilisation d'une notation
mathématique permet une modélisation indépendante de toute
considération
page 42
3.3 Modèle Event-B
informatique. La communauté Event-B étant
très active, et du fait de l'utilisation industrielle de la
méthode, des outils performants sont proposés. Des outils de
preuve et des vérificateurs de modèles (model checkers).
| 
