3.4 Exemple de machine en Event-B
Dans cette section nous présentons un petit exemple
pour illustrer nos propos. Il s'agit d'une machine Event-B modélisant le
comportement d'une horloge. Le modèle contient une variable heure qui
contient l'heure courante, cette variable est un entier naturel compris entre 0
et 23.Un événement TICK fait évoluer l'heure courante et
un autre événement RAZ remet l'heure à zéro quant
celle-ci dépasse 23.L'initialisation met la valeur de l'horloge à
0.
page 48
3.5 RODIN : l'outil support d'Event-B
|
MACHINE horloge VARIABLES heure
INVARIANT Heure E 0..23 INITIALISATION heure := 0 EVENTS
EVENT TICK WHERE
Heure < 23 THEN
Heure := heure + 1 END
EVENT RAZ WHERE
heure = 23 THEN
heure := 0 END
|
3.5 RODIN : l'outil support d'Event-B
Event-B fournit actuellement un logiciel libre sous la forme
d'une plateforme (dérivée de « Eclipse ») de
spécification et de preuve, appelé RODIN [27] [28]. Cette
dernière a été initialement développée dans
le cadre d'un projet européen.
page 49
3.6 Conclusion
La plate-forme Rodin, illustrée dans la Figure 3.3
FIGURE 3.3 - La plateforme RODIN
3.6 Conclusion
D
ans ce chapitre, nous avons présenté d'une
façon rigoureuse les concepts de base de la méthode formelle
Event-B. Une telle méthode permet le développement
pas-à-pas des logiciels corrects par construction.
| 
