4.5 Vérification formelle par l'outil Rodin
Dans cette section, nous présentons comment nous
procédons pour vérifier la cohérence et la
fiabilité du modèle Event-B obtenu. Pour chaque concept et
règle que nous avons formalisé, nous allons montrer comment nous
l'avons prouvés à l'aide des outils de vérifications
fournis par la plateforme RODIN.
~ RODIN : un atelier qui a été
développé dans le cadre d'un projet européen. Il est
basé sur Eclipse. RODIN stocke les modèles dans une base de
données et fournit des nouveaux prouveurs puissants, qui peuvent
être manipulés à l'aide d'une interface graphique.
4.5.1 Preuves d'une machine
Dans une machine Event-B, il est nécessaire de
vérifier que l'état initial (initialisation) satisfait les
invariants. Ainsi, pour un tel évènement il faut s'assurer que
l'action non-déterministe est réalisable. Cela se fait à
l'aide de l'obligation de preuve de faisabilité.
Dans le modèle abstrait les propriétés
souhaitées du système sont exprimées dans les invariants,
il est nécessaire de prouver la cohérence de ces invariants par
rapport aux évènements du système par des preuves.
Une Obligation de Preuve (OP) : est une
formule mathématique à démontrer afin d'assurer qu'un
composant B (CONTEXT ou MACHINE) est correct. Les outils, support la
spécification en Event-B comme Rodin, peuvent générer les
OPs et les prouver.
Corrections guidées par la preuve :
Une OP non prouvée indique une erreur dans le modèle.
Vérification par la preuve : Rodin
génère l'ensemble des OPs nécessaires à la
validation de la cohérence de modèle, et de la
préservation de l'invariant par ce modèle.
Dans notre modèle, nous trouvons des obligations de
preuve Figure 4.32. Chacun d'eux a un nom composé, par exemple, evt /
inv / INV. Un logo vert situé à gauche du nom de l'obligation de
preuve mentionne qu'elle a été prouvée, un A signifie
qu'elle a été prouvée automatiquement.
page 89
4.5 Vérification formelle par l'outil Rodin
FIGURE 4.32 - Les OPs sous Rodin de la
machine
Dans la Figure 4.33, les obligations de preuve
associées à chaque invariant ont été
générer automatiquement. Soit l'exemple suivant : INITIALISATION
/ inv2 / INV. Cette règle d'obligation de preuve assure que l'invariant
inv2, dans la machine, soit préservé par
l'évène-ment INITIALISATION. Cette obligation de preuve a
été déchargée automatiquement par le RODIN
prover.
page 90
4.5 Vérification formelle par l'outil Rodin
FIGURE 4.33 - Preuve automatique
Toutefois, les obligations de preuve produites par les
générateurs de preuve, pourraient exiger une preuve interactive
au lieu de preuves automatiques. Tel est l'exemple, dans la Figure 4.34, de
l'obligation de preuve Deposit / grd1 / THM qui a été
prouvée interactive-ment.
page 91
4.6 Conclusion
FIGURE 4.34 - Preuves interactif
Dans le développement de notre modèle des
obligations de preuve n'ont pas été déchargées par
les outils de preuves automatiques et interactifs, mais les
spécifications sont correctes.
| 
