[LAL02] Conception et développement formels d'applications bases de données
Mémoire de HDR :
Soutenue le: 01 January 2002,
: Conception et développement formels d'applications bases de données,
motcle:
Résumé:
Dans le domaine des systèmes d'information, les données sont modélisées à un haut niveau d'abstraction en utilisant les modèles de type Entité/Association ou relationnel binaire. L'objectif de mes travaux de recherche a été de spécifier
le comportement fonctionnel des transactions d'un SI
au même niveau d'abstraction que les données, en utilisant une méthode de spécifications
formelles existante afin de pouvoir bénéficier de tous les outils
de raisonnement associés. On obtient ainsi une spécification
globale d'un SI dont la cohérence données-traitements est
vérifiée. J'ai montré ensuite qu'il était possible d'aller plus
loin en générant, par un processus de raffinement, une
implémentation relationnelle à partir de la spécification formelle
obtenue. Le processus étant formel, les transactions générées sont
correctes par rapport à la spécification.
Ces travaux ont été réalisés en utilisant la méthode B dont le paradigme de spécification, basé sur les transitions d'états,
est bien adaptée aux types de systèmes et aux types de propriétés
considérés.
Plus récemment, je me suis tournée vers des méthodes formelles qui
permettent d'exprimer et de valider d'autres types de propriétés
que les propriétés fonctionnelles, plus liées à l'aspect dynamique
des SI. Il est alors nécessaire de définir des règles qui
permettent d'assurer la cohérence globale du système.Un autre point qui me paraît intéressant d'étudier concerne la réutilisation de composants de spécification.
Commentaires:
Habilitation à diriger des recherches, Université d'Evry, décembre 2002