Accueil > Manifestations > Thèses et HDR > Thèses > Mohamed El-habib Messabihi

Mohamed El-habib Messabihi

Directeur de thèse

Christian Attiogbé
Pascal André

Résumé

L’utilisation croissante des composants et des services logiciels dans les différents secteurs d’activité
(télécommunications, transports, énergie, fi-nance, santé, etc.) exige des moyens (modèles, méthodes,
outils, etc.) rigoureux a-n de maîtriser leur production et d’évaluer leur qualité. En particulier, il est crucial
de pouvoir garantir leur bon fonctionnement en amont de leur déploiement lors du développement
modulaire de systèmes logiciels.

Kmelia est un modèle à composants multi-services développé dans le but de construire des composants
logiciels et des assemblages prouvés corrects. Trois objectifs principaux sont visés dans cette thèse.
Le premier consiste à enrichir le pouvoir d’expression du modèle Kmelia avec un langage de données afi-n
de satisfaire le double besoin de spéci-fication et de véri-fication. Le deuxième vise l’élaboration d’un cadre de
développement fondé sur la notion de contrats multi-niveaux. L’intérêt de tels contrats est de maîtriser la construction
progressive des systèmes à base de composants et d’automatiser le processus de leur véri-fication. Nous nous
focalisons dans cette thèse sur la véri-fication des contrats fonctionnels en utilisant la méthode B. Le troisième
objectif est l’instrumentation de notre approche dans la plate-forme COSTO/Kmelia. Nous avons implanté un
prototype permettant de connecter COSTO aux différents outils associés à la méthode B. Ce prototype permet
de construire les machines B à partir des spéci-fications Kmelia en fonction des propriétés à vérifier. Nous montrons
que la preuve des spéci-fications B générées garantit la cohérence des spéci-fications Kmelia de départ. Les
illustrations basées sur l’exemple CoCoME confortent nos propositions.

Mots-clés : Modèle de composants, Services, Contrats, Vérifi-cation formelle, Méthode B.

Dernière modification : jeudi 7 juillet 2011