3.3 Modèle Event-B
Le modèle est le premier concept d'Event-B. Il est
composé d'un ensemble des machines et des contextes. Un modèle
Event-B peut contenir des contextes seulement, des machines seulement ou les
deux. Dans le premier cas, le modèle représente une structure
mathématique pure. Le deuxième cas représente un
modèle non paramétré.
3.3.1 Structure d'une Machine
La machine Event-B contient des éléments
dynamiques qui décrivent l'état du système. Une machine
est constituée de trois sections principales : les variables sont
données dans la clause VARIABLES et initialisées dans la clause
Initialisation, aussi les invariants définit l'espace d'état des
variables, et les évènements. La machine est constituée de
plusieurs clauses, ces clauses sont décrites comme suit :
~ MACHINE : La clause MACHINE
représente le nom du composant qui devrait être unique dans un
modèle.
~ SEES : la clause SEES spécifie la
liste des contextes « vus » par la machine. Dans ce cas la machine
peut utiliser les constantes les ensembles et les axiomes figurant dans le
contexte.
~ VARIABLES : définit la liste des
variables introduites dans la machine qui constituent l'état du
système. Les valeurs de ces variables sont initialisées dans
Initialisation et peuvent changer par les évènements.
~ INVARIANTS : sert au typage des variables
et à décrire les contraintes qu'elles doivent respecter sous
forme des prédicats.
~ EVENTS : contient la liste des
événements qui opèrent une ou plusieurs substitutions sur
la valeur des variables. L'événement INTIALISATION donne une
valeur initiale aux variables.
page 43
3.3 Modèle Event-B
3.3.2 Structure d'un Contexte
Un contexte représente la partie statique du
modèle, il est composé de constantes et d'axiomes
décrivant les propriétés de ces constantes. Un contexte
peut être visible pour une machine en utilisant la clause « SEES
».
FIGURE 3.2 - Relation entre un contexte et une
machine
La structure du contexte est constituée d'un ensemble
de clauses introduites par des mots clés, ces clauses sont
décrites comme suit :
~ CONTEXT : représente le nom du
composant qui devrait être unique dans un modèle.
~ SETS : définit les ensembles
porteurs du modèle. Ces ensembles non vides servent à typer le
reste des entités du modèle.
~ CONSTANTS : cette clause contient la liste
des constantes utilisées par le modèle. Dans la suite nous
présentons les constituants d'un évènement Event-B.
3.3.3 Structure d'un Evénement
En Event-B, les événements remplacent les
opérations. Un événement d'initialisation permet de
définir les valeurs initiales des variables. Ces valeurs doivent
établir les invariants. Les autres événements ont des
gardes qui garantissent des propriétés. Les gardes sont
définies dans la clause WHEN et sont mises en conjonction. Si l'une des
gardes d'un événement est fausse, l'événement ne
peut pas être déclenché. Les actions d'un
événement sont exécutées de manière
concurrente, et il n'est pas possible de modifier la même variable dans
deux actions d'un même événement.
page 44
3.3 Modèle Event-B
La structure d'un évènement est
constituée d'un ensemble de clauses introduites par des mots
clés. Ces clauses sont décrites comme suit :
~ ANY : énumèe la liste des paramètres de
l'évènement.
~ WHERE : contient les différentes
gardes de l'évènement. Ces gardes sont des conditions
nécessaires pour déclencher l'évènement. Il faut
noter que si la clause « any » est omise le mot clé «
where » est remplacé par « when ».
~ WITH : lorsqu'un paramètre abstrait
disparait dans la version concrète de cet évènement, il
est indispensable de définir un témoin sur l'existence de ce
paramètre. ~ THEN : décrit la liste des actions
de l'évènement.
3.3.3.1 Les différentes formes des
événements
Les évènements, dans Event-B, peuvent avoir
l'une des trois formes : indéterminée, gardée ou simple.
La sémantique formelle d'un évènement s'exprime à
partir de la sémantique de la substitution autrement dit la relation qui
existe entre la valeur des variables avant et après le
déclenchement de l'évènement.
La première est la forme dite
indéterministe où x est une variable
d'état du système et t une variable locale.
L'évènement ne se déclenche que s'il existe une
valeur de la variable t qui satisfait le prédicat G(x, t).x : P (x', x,
t) est l'action de l'évènement. La présence de la variable
locale t fait que cet évènement est non
déterministe.
EVENT nom
ANY
t
WHERE
G(x, t)
THEN
x : P(x,
x0, t)
END
page 45
3.3 Modèle Event-B
La seconde forme est celle dite gardée
dans laquelle il n'y a pas de variable locale et où la garde et
l'action ne dépendent que des variables d'états du
modèle.
EVENT nom
WHEN
G(x)
THEN
x : P(x, x0)
END
La forme simple inclut seulement une action. Cela équivaut
donc à une garde qui est toujours vraie.
EVENT nom
BEGIN
x : P(x, x0)
END
Il existe aussi un évènement avec une action et
une garde vide : l'évènement skip. Rappelons qu'il existe un
évènement obligatoire, nommé INITIALISATION, qui est
toujours de la forme simple. A la différence d'un véritable
évènement, cet évènement permet d'initialiser le
système en spécifiant les valeurs initiales possibles (qui
doivent bien sûr respecter les invariants).
Avant de passer aux obligations de preuve d'un modèle
B, il faut présenter les prédicats avant-après des
événements traditionnellement notés BA (pour before after
en anglais). Ces prédicats définissent la relation entre la
valeur des variables d'état avant et après le
déclenchement des événements. La valeur d'une variable x
après le déclenchement d'un événement est
notée x'. Par exemple le prédicat avant-après de
l'événement TICK de la machine HORLOGE est heure' = heure+1.Le
tableau 3.1 résume les prédicats avant-après selon la
forme des événements.
page 46
3.3 Modèle Event-B
TABLE 3.1 - prédicats avant-après
3.3.3.2 Obligations de preuves
Les obligations de preuve définissent ce que doit
être prouvée pour un modèle Event-B. Ils sont
générés automatiquement par un générateur
d'obligations de preuve. Ce générateur vérifie les
machines et les contextes et il décide ce que doit être
prouvé dans ces machines et contextes.
Nous décrivons dans ce qui suit les obligations de
preuve associées à une machine abstraite d'un modèle
Event-B.
L'obligation de preuve de
préservation de l'invariant : INV
Cette obligation de preuve assure que chaque invariant d'une
machine soit préservé par chaque évènement. Pour un
évènement evt et un invariant inv (x), l'obligation de preuve
associée est "evt / inv / INV". Si I(x) est l'invariant du
système, alors pour tout évènement E du système qui
a comme prédicat avant-après BA l'obligation de preuve est comme
suit:
I(x)?BA(x, x') =
I(x')
Par rapport à notre exemple l'obligation de preuve est la
suivante :
|
Heure E 0..23 heure < 23
F-
heure := heure + 1
|
page 47
3.4 Exemple de machine en Event-B
L'obligation de preuve de Faisabilité :
FIS
Le but de cette obligation de preuve est de s'assurer que
l'action non-déterministe est réalisable. Pour un
évènement evt et une action act l'obligation de preuve
associée est "evt/act/-FIS". I étant l'invariant du
système, alors l'obligation de preuve qui correspondant à un
évènement E est comme suit :
I (x)?grd(E) = x'.P(x,
x')
Heure E 0..23 heure < 23
F-
?i.i E 0..23 ?i := heure + 1
Par rapport à notre exemple l'obligation de preuve est la
suivante :
| 
