ITERATION 0
Le premier exemple traité ici n'a pas d'autre intérêt que d'illustrer le concept de raffinement temporel. Cette notion est certainement la moins évidente à appréhender quand on débute sur la méthode.
Le système à représenter est constitué d'une porte et d'une fenêtre.
Il est important de se rappeler qu'un modèle B système (ou Event-B) ne décrit pas le système mais une observation de celui-ci.
Un tel modèle comporte trois types d'objets :
- des variables
- des propriétés invariantes
- des évènements.
Variables :
Nous allons à l'aide de variables représenter les éléments du système dont nous souhaitons observer l'évolution, et ce le plus simplement possible. Nous avons une porte et une fenêtre à modéliser. Nous allons considérer seulement deux états pour cette porte et cette fenêtre : ouvert et fermé. Plutôt que de définir un type composé de ces deux valeurs "ouvert" et "fermé" nous allons faire plus simple en considérant deux booléens baptisés p et f (pour porte et fenêtre). Par convention, p sera vrai si la porte est ouverte, et fausse si elle fermée. Idem pour f.
Propriétés invariantes :
Nous avons précisé auparavant qu'un modèle représente une observation du système que l'on cherche à représenter. Il est fondamental de comprendre que l'observateur de ce système en fonctionnement conserve toujours ses yeux fermés sauf en certains instants bien choisis. Ainsi, dans le cas présent, et dans un premier temps, nous allons considérer que l'observateur n'ouvre les yeux qu'à deux instants, choisis de telle sorte qu'ils permettent à l'observateur de visualiser ce qui suit :
- la porte et la fenêtre sont fermées,
- la porte et la fenêtre sont ouvertes.
Ce choix des instants d'observation étant fait, il nous est alors possible de définir l'ensemble des propriétés invariantes qui sont :
- "p est un booléen"
- "f est un booléen"
- "p et f sont vrais simultanément ou faux simultanément"
Evènements :
Un événement caractérise l'écart observé entre deux instants d'observation consécutifs. Nous allons donc considérer les deux évènements suivants : "ouvrir porte et fenêtre" et "fermer porte et fenêtre". Ces deux évènements correspondent aux transitions observables suivantes :
- (porte fermée, fenêtre fermée) ==> (porte ouverte, fenêtre ouverte)
- (porte ouverte, fenêtre ouverte) ==> (porte fermée, fenêtre fermée)
Nous allons maintenant mettre en forme cette modélisation en utilisant un atelier. Deux options sont possibles : l'atelier B (ici) et RODIN (ici).
MODELE OBTENU :
Avec RODIN, nous obtenons, après export vers latex et conversion en PDF, le modèle suivant baptisé "M00" (Machine numéro 00)
Nous comprenons qu'un tel système est supposé pouvoir perdurer dans le temps et jamais donc se retrouver dans un état de blocage. Il convient de le vérifier au niveau du modèle obtenu.
Nous devons simplement vérifier que la disjonction des gardes des deux évènements est toujours vraie.
En l'occurrence, nous avons "(p est faux et f est faux) ou (p est vraie et f est vraie)". compte tenu de l'invariant inv3 établi, nous pouvons conclure que ce modèle ne se bloque jamais.
ITERATION 1
Dans un second temps, nous allons observer plus finement le système considéré. En fait, pas de raffinement spatial à considérer puisque les objets du système sont déjà représentés au juste niveau d'abstraction nécessaire. Nous allons simplement observer le système "plus souvent" que précédemment en ajoutant deux instants d'observation supplémentaires. Le premier de ces deux instants est choisi de telle sorte que l'observateur visualise la scène où la porte est fermée et la fenêtre ouverte. Le second est choisi de telle sorte que l'observateur visualise la scène où la porte est ouverte et la fenêtre est fermée.
Transitions possibles observables désormais :
- (porte fermée, fenêtre fermée) ==> (porte ouverte, fenêtre fermée)
- (porte ouverte, fenêtre fermée) ==> (porte ouverte, fenêtre ouverte)
- (porte ouverte, fenêtre ouverte) ==> (porte fermée, fenêtre ouverte)
- (porte fermée, fenêtre ouverte) ==> (porte fermée, fenêtre fermée)
- (porte fermée, fenêtre fermée) ==> (porte fermée, fenêtre ouverte)
- (porte fermée, fenêtre ouverte) ==> (porte ouverte, fenêtre ouverte)
- (porte ouverte, fenêtre ouverte) ==> (porte ouverte, fenêtre fermée)
- (porte ouverte, fenêtre fermée) ==> (porte fermée, fenêtre fermée)
Nous allons donc considérer 8 évènements au lieu de 2 auparavant.
Nous choisissons de mémoriser la dernière action faite (c'est-à-dire une action parmi les 4 suivantes : ouverture porte, fermeture porte, ouverture fenêtre, fermeture fenêtre) dans le but de pouvoir tracer les enchainements de deux évènements consécutifs. Certains de ces enchaînements vont pouvoir, en effet, être considérés comme des raffinements des évènements abstraits identifiés dans M00.
Ci-dessous sont listés les 8 enchaînements possibles de 2 transitions, ces enchaînements commençant par l'un des deux états considérés dans M00. Ces enchaînements sont volontairement regroupés par deux :
- Le premier enchaînement représente un couple de transitions pour lequel l'état de fin et l'état de début sont identiques et connus dans M00
- Le second enchaînement représente un couple de transitions pour lequel les états de début et de fin sont distincts et connus dans M00,
- pour les deux enchaînements, la seconde transition est identique.
- (porte ouverte, fenêtre ouverte) ==> (porte ouverte, fenêtre fermée)
- (porte ouverte, fenêtre fermée) ==> (porte ouverte, fenêtre ouverte)
et
- (porte fermée, fenêtre fermée) ==> (porte ouverte, fenêtre fermée)
- (porte ouverte, fenêtre fermée) ==> (porte ouverte, fenêtre ouverte)
puis,
- (porte ouverte, fenêtre ouverte) ==> (porte fermée, fenêtre ouverte)
- (porte fermée, fenêtre ouverte) ==> (porte ouverte, fenêtre ouverte)
et
- (porte fermée, fenêtre fermée) ==> (porte fermée, fenêtre ouverte)
- (porte fermée, fenêtre ouverte) ==> (porte ouverte, fenêtre ouverte)
puis,
- (porte fermée, fenêtre fermée) ==> (porte ouverte, fenêtre fermée)
- (porte ouverte, fenêtre fermée) ==> (porte fermée, fenêtre fermée)
et
- (porte ouverte, fenêtre ouverte) ==> (porte ouverte, fenêtre fermée)
- (porte ouverte, fenêtre fermée) ==> (porte fermée, fenêtre fermée)
puis,
- (porte fermée, fenêtre fermée) ==> (porte fermée, fenêtre ouverte)
- (porte fermée, fenêtre ouverte) ==> (porte fermée, fenêtre fermée)
et
- (porte ouverte, fenêtre ouverte) ==> (porte fermée, fenêtre ouverte)
- (porte fermée, fenêtre ouverte) ==> (porte fermée, fenêtre fermée)
Pour chacune de ces 4 paires d'enchainements, le second enchaînement matérialise le passage de l'état (porte ouverte, fenêtre ouverte) vers l'état (porte fermée, fenêtre fermée) ou l'inverse.
Ces 4 enchaînements correspondent donc, suivant le cas, à l'un des deux évènements identifiés dans M00.
Ainsi :
L'enchaînement
- (porte fermée, fenêtre fermée) ==> (porte ouverte, fenêtre fermée)
- (porte ouverte, fenêtre fermée) ==> (porte ouverte, fenêtre ouverte)
est à associer à l'évènement abstrait "ouvrir_porte_et_fenêtre".
L'enchaînement
- (porte fermée, fenêtre fermée) ==> (porte fermée, fenêtre ouverte)
- (porte fermée, fenêtre ouverte) ==> (porte ouverte, fenêtre ouverte)
est à associer à l'évènement abstrait "ouvrir_porte_et_fenêtre".
L'enchaînement
- (porte ouverte, fenêtre ouverte) ==> (porte ouverte, fenêtre fermée)
- (porte ouverte, fenêtre fermée) ==> (porte fermée, fenêtre fermée)
est à associer à l'évènement abstrait "fermer_porte_et_fenêtre".
L'enchaînement
- (porte ouverte, fenêtre ouverte) ==> (porte fermée, fenêtre ouverte)
- (porte fermée, fenêtre ouverte) ==> (porte fermée, fenêtre fermée)
est à associer à l'évènement abstrait "fermer_porte_et_fenêtre".
Pour distinguer ces 4 enchaînements des autres, des variables booléennes ont été ajoutées. Elles ont pour but unique de mémoriser la dernière action précédente effectuée :
- ouverture porte,
- fermeture porte,
- ouverture fenêtre,
- fermeture fenêtre.
La méthode nous impose la règle suivante : aucune variable abstraite ne peut être modifiée par un évènement concret si elle n'a pas été modifiée par l'événement abstrait correspondant (le terme "concret" permet de désigner un objet du dernier modèle obtenu dans la suite des raffinements, alors que le terme "abstrait" permet de désigner un objet de l'avant-dernier modèle dans la suite des raffinements).
C'est pour cette raison que les variables p et f ont été remplacées par les variables p2 et f2.
- p2 et f2 représentent l'état de la porte et de la fenêtre à chacun des 4 instants d'observation.
- p et f représentent l'état de la porte et de la fenêtre à chacun des 2 instants d'observation considérés dans M00.
La dernière action effectuée est représentée par les 4 booléens suivants :
- of ("ouverture fenêtre")
- op ("ouverture porte")
- ff ("fermeture fenêtre")
- fp ("fermeture porte")
A chacun des 4 instants d'observation du système, une seule de ces 4 variables est vraie. Cela nous conduit à spécifier les 4 propriétés invariantes suivantes :
- "si of est vrai alors op, ff, fp sont faux"
- "si op est vrai alors ff, fp, of sont faux"
- "si ff est vrai alors fp, of, op sont faux"
- "si fp est vrai alors of, op, ff sont faux"
Il nous reste à établir les propriétés invariantes de liaison. Ces propriétés relient les variables abstraites p et f aux variables concrètes p2 et f2.
Aux deux instants d'observation préalablement identifiés dans M00, on a :
- "Si p2 et f2 sont vrai alors f et p sont vrai"
- "Si p2 et f2 sont faux alors f et p sont faux"
(les propriétés sont formulées pour être valables sur les 4 instants d'observation)
Aux deux nouveaux instants d'observation identifiés ici, on a :
- "si p2 est vrai et si op est faux alors p est vrai"
- "si f2 est vrai et si of est faux alors f est vrai"
- "si p2 est faux et si fp est faux alors p est faux"
- "si f2 est faux et si ff est faux alors f est faux"
(les propriétés sont formulées pour être valables sur les 4 instants d'observation).
On s'aperçoit après coup que les 4 dernières propriétés invariantes de liaison formulées impliquent les deux précédentes. Les deux précédentes peuvent donc être retirées.
MODELE OBTENU
Concernant l'absence de blocage du modèle, il nous suffit de vérifier (sous hypothèse que les invariants sont vraies) :
(p2 = FALSE and f2 = FALSE) or
(p2 = TRUE and f2 = TRUE) or
(f2 = TRUE and p2 = FALSE and of = TRUE) or
(f2 = TRUE and p2 = FALSE and of = FALSE) or
(p2 = TRUE and f2= FALSE and op = TRUE) or
(p2 = TRUE and f2 = FALSE and op = FALSE) or
(f2 = FALSE and p2 = TRUE and ff = TRUE) or
(f2 = FALSE and p2 = TRUE and ff = FALSE) or
(p2 = FALSE and f2 = TRUE and fp = TRUE) or
(p2 = FALSE and f2 = TRUE and fp = FALSE)
ce qui est équivalent à :
(p2 = FALSE and f2 = FALSE) or
(p2 = TRUE and f2 = TRUE) or
(f2 = TRUE and p2 = FALSE) or
(p2 = TRUE and f2= FALSE) or
(f2 = FALSE and p2 = TRUE) or
(p2 = FALSE and f2 = TRUE)
ce qui est équivalent à :
(p2 = FALSE) or
(p2 = TRUE) or
(f2 = TRUE and p2 = FALSE) or
(f2 = FALSE and p2 = TRUE)
ce qui est toujours vrai.
ITERATION 2
Ici des évènements sont fusionnés pour simplifier le modèle.
Pour fusionner deux évènements en un seul, il faut et il suffit que les actions soient identiques.
La garde du nouvel évènement est égale à la disjonction des gardes des évènements initiaux.
MODELE OBTENU
ITERATION 3
Ici les variables inutiles sont éliminées. Il s'agit de op, fp, of et ff.
Elles avaient été introduites pour permettre de certifier que M01 était un raffinement de M00.
MODELE OBTENU
On peut noter que le modèle obtenu aurait pu être établi directement en une seule étape au lieu de 4 comme on l'a fait ici. Mais dans un exemple plus complexe de système, la modélisation en une seule étape ne sera généralement plus possible.