B événementiel de J.R. Abrial

Source : Présentation de J.R. Abrial (Janvier 2000)
 
Le contrôleur du pont de l'île
Le principe : le saut en parachute.

Plus on s'approche du sol, plus on voit de choses, plus on voit d'événements.

Première vue du système (ou modèle initial)
Quelles sont les données ?
On a une seule variable, n, le nombre de véhicules qui sont dans le système.
De plus, le nombre maximum de véhicules que peut contenir le système est constant (d)
La contrainte à satisfaire est :

0 <= n <= d

La forme générale d'un événement pour cette présentation
 

==
    WHEN
       < garde>
    THEN
    < action>
    END

On a deux événements
Sortie du continent vers le système
 

ML_OUT ==
    WHEN
        n < d
    THEN
        n := n+ 1
    END

Entrée sur le continent
 

ML_IN ==
    WHEN
        n > 0
    THEN
        n := n - 1
    END

Les obligations de preuve
1) La préservation de l'invariant
 

Etant donné un événement de forme générale : EVENT ==
    WHEN
        G(x)
    THEN
        x := E(x)
    END
et un invariant I(x) à préserver, il faut prouver que :
I(x) & G(x) => I(E(x))
 

Soit dans notre cas
pour l'événement ML_OUT
0 <= n <= d & n 0 <= n + 1 <= d
pour l'événement ML-IN
0 <= n <= d & n 0 <= n - 1 <= d
2) Preuve de vivacité (liveness)
 

 Etant donné un système d'événements avec les gardes :
G1 (x), ..., Gn (x) et un invariant I(x), l'énoncé à prouver est :
I(x) => G1(x) or ...or Gn(x)
i.e. un événement au moins est toujours prêt à être déclenché (ABSENCE DE VERROU FATAL)

Soit ici :
0 <= n <= d => 0 < n or n < d
Ce que l'on ne peut prouver !
Quand n = 0, on ne peut prouver n < d
On a oublié 0 < d
Il y a un deadlock si d = O (plus aucune voiture ne peut entrer).
On corrige donc et alors on peut prouver que :
 
0 <= n <= d  & 0 < d => 0 < n or n < d
3) Preuve d'absence de sous-boucles infinies
Pour chaque événement (dans le cas de deux événements seulement) :
 

EVENT ==
    WHEN G(x) THEN x := E(x) END Il faut prouver, étant donné un invariant I(x) :
I(x) => 0 <= V(x) &
I(x) & G(x) =< V (E(x)) < V(x)
où V(x) est un variant à exhiber pour chaque événement.

Soit ici
Pour ML_OUT, un variant est d - n
0 <= n <= d & 0 < d => 0 <= d - n
0 <= n <= d & 0 < d & n < d
=>
d - (n + 1) < d - n
Pour ML_IN, un variant est n
0 <= n <= d & 0 < d => 0 <= n
0 <= n <= d & 0 < d & n < d
=>
n -1 <  n
Deuxième vue du système , raffinage par introduction du pont
On est descendu  et on aperçoit maintenant le pont.
On voit :
 

- des véhicules sur le pont qui se dirigent vers l'île (un nombre n)
- des véhicules qui sont dans l'île (un nombre b)
- des véhicules qui se dirigent vers le contenant (un nombre c)

L'invariant
 

0 <= a &
0 <= b &
0 <= c &
a = 0 or c = 0 /* tous les véhicules vont dans la même direction */

Invariant de collage
 

a + b + c = n

Les techniques de raffinage :
 

1) Chaque événement est raffiné par un événement concret 2) Le monde abstrait travaille avec x et le concret avec y
3) Un invariant de collage I(x, y) lie les deux mondes

Les mécanismes de raffinage sont :
 

- le renforcement des gardes (normal, plus on voit de choses en s'approchant du sol, plus on voit de contraintes. C'est bien connu, quand on est "haut placé" on est en dehors des contingences matérielles...voilà sans doute pourquoi certains recherchent ces places...dans les amphis (?!))     Rappel : en ce qui concerne les préconditions, on les affaiblit lors du raffinage.
- des actions "simultanées" sur l'invariant de collage.

Dans notre cas,
1) Raffinage de l'événement abstrait
ML_OUT == WHEN n < d THEN n := n + 1 END
en :
ML_OUT ==
    WHEN
        a + b + c < d & c = 0  /* On a renforcé la garde */
    THEN
        a := a + 1
    END
Raffinage de l'autre événement abstrait :
ML_IN ==
    WHEN
        n > 0
    THEN
        n := n + 1
    END
en :
ML_IN ==
        WHEN
            c > 0
        THEN
            c := c - 1
        END
2) Spécification des nouveaux événements
IL_IN ==
    WHEN
        a > 0
    THEN
        a, b := a - 1, b + 1
    END
IL_OUT ==
    WHEN
        b > 0 &
        a = 0
    THEN
        b, c := b - c, c + 1
    END
Les obligations de preuve du raffinage d'événement
 

Etant donné un événement abstrait  et un événement concret correspondant EVENT == WHEN G(x) THEN x := E(x) END
EVENT == WHEN H(y) THEN y := F(y) END
et les invariant I(x) (supposé être déjà préservé par l'événement abstrait) et J(x, y),
I(x) & J(x, y) & H(y) => G(x)
I(x) & J(x, y) & H(y) => J(E(x), F(y))

...
à vous maintenant d'appliquer cela...
Les niveaux suivants seront :
1) Introduction de deux feux de circulation à chaque entrée du pont
2) Introduction de capteurs  (il faut bien compter les véhicules pour vérifier l'invariant fourni au premier niveau) à l'entrée et à la sortie du pont
Puis introduction du contrôleur qui :
 

- décide quand les feux doivent changer
- n'a pas accès aux variables physiques
- a accès à des variables de contrôle
- qui sont des copies de variables physiques

    - qui représentent ce que le contrôleur croit de la situation physique
    - dont les valeurs peuvent être différentes de celles des variables physiques
            mais néanmoins le système doit fonctionner correctement comme celà est prescrit par les vairiables physiques
- conservées en mémoire du contrôleur
3) Introduction des canaux de communication
        - entre le monde physique et le contrôleur (annonce de l'arrivée ou du départ d'un véhicule)
        - entre le contrôleur et le monde physique (pour faire changer)
Des hypothèses temporelles doivent être faites (par exemple que les capteurs physiques sont moins réactifs que les autres événements)
4) Réunion des variables physiques et des variables canaux pour former une seule entité, l'environnement fait de :
        - des variables physiques et des variables canaux
        - tous les événements physiques
        - deux services d'entrée/sortie