Illustrations de la mise en oeuvre de la méthode B système (Event-B)

Ces pages ont pour vocation d'illustrer par quelques exemples concrets l'intérêt de la méthode B système pour spécifier / concevoir des architectures de systèmes discrets. La méthode est très bien présentée par son auteur (J.R. Abrial) sur un ouvrage de près de 600 pages. Je vous recommande donc sa lecture si vous ressentez l'envie ou le besoin de franchir un nouveau palier dans le domaine de l'ingénierie de systèmes discrets. Vous trouverez la référence du livre ici.

Les concepts introduits par cette méthode sont en nombre limité mais puissants. C'est une méthode généraliste adaptée à tout système discret. Elle intègre notamment une théorie du raffinement dont le but est de permettre d'appréhender la complexité des systèmes à représenter. Deux types de raffinements : le raffinement spatial et le raffinement temporel. 

1- Un premier exemple ici illustre le raffinement temporel. Il s'agit d'observer un ensemble formé d'une porte et d'une fenêtre qui sont tour à tour ouvertes et fermées. Cet exemple est suffisamment simple pour permettre de mettre l'accent sur cette notion de raffinement temporel.

2- Un second exemple (en cours de construction) illustre la notion de modèle générique dont l'intérêt est de pouvoir servir à différents cas d'étude. Le cas étudié est la réplication d'un processus.

3- A suivre ...

Nota :

Le terme "insyp" veut dire "ingénierie système prouvée"

Ces pages sont destinées à être enrichies au fur et à mesure.

Les preuves ne sont pas présentées mais elles ont été établies avec l'atelier utilisé.