Contribution à la spécification et à la vérification des logiciels à base de composants : enrichissement du langage de données de Kmelia et vérication de contrats

Résumé : L'utilisation croissante des composants et des services logiciels dans les différents secteurs d'activité (télécommunications, transports, énergie, finance, santé, etc.) exige des moyens (modèles, méthodes, outils, etc.) rigoureux afin 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 afin de satisfaire le double besoin de spécification et de vérification. 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érification 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écifications Kmelia en fonction des propriétés à vé- rifier. Nous montrons que la preuve des spécifications B générées garantit la cohérence des spécifications Kmelia de départ. Les illustrations basées sur l'exemple CoCoME confortent nos propositions.
Type de document :
Thèse
Génie logiciel [cs.SE]. Université de Nantes, 2011. Français
Liste complète des métadonnées

Littérature citée [102 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01146895
Contributeur : Christian Attiogbé <>
Soumis le : mercredi 29 avril 2015 - 12:49:26
Dernière modification le : jeudi 5 avril 2018 - 10:36:49
Document(s) archivé(s) le : lundi 14 septembre 2015 - 15:21:07

Identifiants

  • HAL Id : tel-01146895, version 1

Collections

Citation

El-Habib Mohamed Messabihi. Contribution à la spécification et à la vérification des logiciels à base de composants : enrichissement du langage de données de Kmelia et vérication de contrats. Génie logiciel [cs.SE]. Université de Nantes, 2011. Français. 〈tel-01146895〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

408