LogoLogo

Siala, Badr. Décomposition formelle des spécifications centralisées Event-B : application aux systèmes distribués BIP

Siala, Badr (2017). Décomposition formelle des spécifications centralisées Event-B : application aux systèmes distribués BIP.

[img]PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
3112Kb

Résumé en francais

Cette thèse a pour cadre scientifique la décomposition formelle des spécifications centrali- sées Event-B appliquée aux systèmes distribués BIP. Elle propose une démarche descendante de développement des systèmes distribués corrects par construction en combinant judicieu- sement Event-B et BIP. La démarche proposée comporte trois étapes : Fragmentation, Dis- tribution et Génération de code BIP. Les deux concepts clefs Fragmentation et Distribution, considérés comme deux sortes de raffinement automatique Event-B paramétrées à l'aide de deux DSL appropriés, sont introduits par cette thèse. Cette thèse apporte également une contribution au problème de la génération de code à partir d'un modèle Event-B issu de l'étape de distribution. Nous traitons aussi bien les aspects architecturaux que comportemen- taux. Un soin particulier a été accordé à l'outillage et l'expérimentation de cette démarche. Pour y parvenir, nous avons utilisé l'approche IDM pour l'outillage et l'application Hôtel à clés électroniques pour l'expérimentation.

Sous la direction du :
Directeur de thèse
Bodeveix, Jean-Paul
Bhiri, Mohamed Tahar
Filali, Mamoun
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Méthodes formelles - Décomposition formelle - Systèmes distribués - Raffinement automatique - Génération de code - IDM - DSL - Event-B - BIP
Sujets :Informatique
Déposé le :15 Jun 2018 13:43