Thèse de Frédéric Gervais
Titre de la thèse :
Combinaison de spécifications formelles pour la modélisation des systèmes d'information
Directeurs de thèse :
- Régine Laleau, Professeure à l'Université Paris 12
- Marc Frappier, Professeur à l'Université de Sherbrooke (Québec)
- Véronique Donzeau-Gouge, Professeure au CNAM Paris,
Directrice Scientifique Adjointe au Département ST2I du CNRS
Résumé de la thèse :
L'objectif de cette thèse est de profiter des avantages de deux
formes de modélisation complémentaires pour
représenter de manière formelle les systèmes
d'information (SI). Un SI est un système informatisé qui
permet de rassembler les informations d'une organisation et qui fournit
des opérations pour les manipuler. Les SI
considérés sont développés autour de
systèmes de gestion de bases de données (SGBD). Notre
motivation est d'utiliser des notations et des techniques formelles
pour les concevoir, contrairement aux méthodes actuelles qui
sont au mieux semi-formelles. D'une part, EB3 est un langage
formel basé sur les traces d'événements qui a
été défini pour spécifier des SI. D'autre part, B est
un langage formel basé sur les états qui se prête
bien à la spécification des propriétés
statiques des SI. Nous avons défini une nouvelle approche,
appelée EB4, qui bénéficie à la fois des avantages d'EB3 et B. Dans un premier temps, les processus décrits en EB3
sont utilisés pour représenter et pour valider le
comportement du système. Ensuite, la spécification est
traduite en B pour spécifier et vérifier les principales
propriétés statiques du SI. Enfin, nous avons
défini des techniques de synthèse automatique de
transactions BD relationnelles à partir du modèle de
données d'EB3 pour compléter le cycle de développement du SI.
Laboratoires d'accueil :
- Centre d'Etude et de Recherche en Informatique du CNAM (CEDRIC), à l'ENSIIE, à Evry, en France
- Groupe de Recherche en Ingénierie du Logiciel (GRIL) du
Département d'Informatique, à l'Université de
Sherbrooke (Québec), au Canada
Document :
Cette thèse
a été réalisée dans le cadre d'une cotutelle
France/Québec entre le CNAM et l'Université de Sherbrooke (Québec).
Date et lieu de soutenance :
le lundi 4 décembre 2006, à 15h, à l'
ENSIIE, à Evry (Essonne), en salle 302
Composition du jury :
|
Directeurs de thèse :
|
Véronique DONZEAU-GOUGE, Professeure au CNAM, à Paris |
|
Marc FRAPPIER, Professeur à l'Université de Sherbrooke (Québec), au Canada |
|
Régine LALEAU, Professeure à l'Université Paris 12, à Créteil |
|
Rapporteurs :
|
Yves LEDRU, Professeur à l'Université Joseph Fourier, à Grenoble |
|
Ali MILI, Professeur au New Jersey Institute of Technology, aux Etats-Unis |
|
Examinateurs :
|
Isabelle COMYN-WATTIAU, Professeure au CNAM, à Paris |
|
Richard ST-DENIS, Professeur à l'Université de Sherbrooke (Québec), au Canada |
|
Anatol SLISSENKO, Professeur à l'Université Paris 12, à Créteil |
Mentions obtenues :
- Très honorable au CNAM
- Excellente à l'Université de Sherbrooke