3 La méthode formelle Event-B
Sommaire
3.1 Introduction 40
3.2 Quelques langages formels 40
3.2.1 Le langage Z 40
3.2.2 La méthode B 41
3.2.3 La méthode Event-B 41
3.3 Modèle Event-B 42
3.3.1 Structure d'une Machine 42
3.3.2 Structure d'un Contexte 43
3.3.3 Structure d'un Evénement 43
3.4 Exemple de machine en Event-B 47
3.5 RODIN : l'outil support d'Event-B
48
3.6 Conclusion 49
page 40
3.1 Introduction
3.1 Introduction
B
ien que les méthodes formelles demandent des efforts
importants dans leur mise en oeuvre et qu'elles soient consommatrices de temps,
les études ont montré l'intérêt de leur utilisation
lors de chacune des phases du cycle de développement logiciel pour aider
à structurer le raisonnement et apporter des garanties sur le
développement.
Ce chapitre est composé de quatre sections. La
première section présente un aperçu sur quelques langages
formels. La deuxième section présente la structure d'une machine,
d'un contexte et d'un Evénement. La troisième section
présente un exemple de machine en Event-B. Enfin, la quatrième
section présente la plateforme de développement RODIN.
3.2 Quelques langages formels
Les méthodes formelles sont des techniques qui peuvent
être utilisées lors de chacune des phases du cycle de
développement logiciel pour aider à structurer le raisonnement et
apporter des garanties sur le développement. Pour cela, ces
méthodes reposent sur un raisonnement mathématique rigoureux
fondé sur un langage formel.
Les langages formels servent à spécifier de
manière mathématique, via la théorie des ensembles et la
logique de prédicat du premier ordre, un système complexe.
3.2.1 Le langage Z
Le langage Z est un langage pour exprimer les
spécifications formelles de systèmes informatiques [22]. La
notation de langage Z s'inspire de la formalisation de la théorie de
ensembles et de la théorie du premier ordre. Il est basé sur la
notation d'un schéma qui se compose d'une collection d'objets
nommés variables et spécifiés par certains axiomes. Le
schéma est une unité de spécification de Z, encapsule une
partie déclaration et une partie contrainte, comme le montre la Figure
3.1.
page 41
3.2 Quelques langages formels
FIGURE 3.1 - L'unité de
spécification de Z
Le schéma illustré par la Figure 3.1
représente une boite contenant des descriptions utilisant les notations
Z. Les schémas sont utilisés pour décrire les états
d'un système, les états initiaux ou bien les
opérations.
3.2.2 La méthode B
La méthode B est une méthode de
spécification formelle permettant de décrire un système de
son analyse à son implémentation [1] [2]. Son formalisme s'appuie
sur des notations mathématiques utilisant la théorie des
ensembles et la logique du premier ordre pour spécifier à la fois
le système et ses propriétés. La méthode B se base
sur le concept de machine abstraite représentant le système.
Cette machine abstraite décrivant le comportement général
est détaillée au fur et à mesure de la modélisation
pour devenir plus concrète et plus proche de 1'implémentation
finale du système. Ce processus est appelé raffinement. Il joue
un rôle central dans la méthode B. Les étapes de
raffinement sont prouvées afin de garantir que les modèles
successifs modélisent le même système et qu'aucune erreur
n'est introduite lors de la modélisation. De nombreux outils comme
l'atelier B, les éprouveurs B ou ProB [30] appuient le
développement de systèmes avec la méthode B.
| 
