[GER02] Réutilisation de composants de spécification en B
Autres :
motcle:
Résumé:
Afin de factoriser le travail de spécification,
les approches semi-formelles telles que UML
proposent des composants dédiés à des domaines
particuliers. Ces composants mémorisent un
savoir-faire : ils décrivent une solution à un
problème donné, ainsi que le contexte dans lequel
cette solution s'applique. De plus, ils sont
suffisamment génériques afin d'être réutilisés
de nombreuses fois. Dans ce rapport, nous nous
intéressons plus particulièrement aux composants
utilisés pour concevoir des applications : les
patterns. Cette notion de composant réutilisable
manque cependant d'une sémantique précise ainsi
que de consensus sur un formalisme de description.
L'objectif du stage était d'adapter la notion de
pattern à la méthode B, afin de bénéficier aussi
bien des avantages d'une approche formelle telle
que B que ceux des composants réutilisables
comme les patterns UML.
Après un bref état de l'art sur la réutilisation
de composants, nous proposons dans ce rapport
une manière de définir un composant de
spécification et une solution pour
instancier de tels composants en B. En utilisant
uniquement les mécanismes existant en B, comme
l'inclusion et le raffinement, la
solution proposée pour instancier les composants
de spécification permet en outre de valider
les spécifications B de l'instance obtenue
grâce aux mécanismes de preuve de la méthode B.
Ce stage de DEA, réalisé au sein de l'équipe CPR
du CEDRIC de l'IIE, a été encadré par Sandrine
Blazy et Régine Laleau.
Commentaires:
Rapport de stage, DEA Informatique, Université d'Evry, Juillet 2002.