LogoLogo

Graja, Zaineb. Vérification formelle des systèmes multi-agents auto-adaptatifs

Graja, Zaineb (2015). Vérification formelle des systèmes multi-agents auto-adaptatifs.

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

Résumé en francais

Un des défis majeurs pour le développement des Systèmes Multi-Agents (SMA) auto-organisateurs est de garantir la convergence du système vers la fonction globale attendue par un observateur externe et de garantir que les agents sont capables de s'adapter face aux perturbations. Dans la littérature, plusieurs travaux se sont basés sur la simulation et le model-checking pour analyser les SMA auto-organisateurs. La simulation permet aux concepteurs d'expérimenter plusieurs paramètres et de créer certaines heuristiques pour faciliter la conception du système. Le model-checking fournit un support pour découvrir les blocages et les violations de propriétés. Cependant, pour faire face à la complexité de la conception des SMA auto-organisateurs, le concepteur a également besoin de techniques qui prennent en charge non seulement la vérification, mais aussi le processus de développement lui-même. En outre, ces techniques doivent permettre un développement méthodique et faciliter le raisonnement sur divers aspects du comportement du système à différents niveaux d'abstraction. Dans cette thèse, trois contributions essentielles ont été apportées dans le cadre du développement et la vérification formelle des SMA auto-organisateurs: une formalisation à l'aide du langage B-événementiel des concepts clés de ces systèmes en trois niveaux d'abstraction (micro, méso et macro), une expérimentation d'une stratégie de raffinement descendante pour le développement des SMA auto-organisateurs et la proposition d'un processus de raffinement ascendant basé sur des patrons de raffinement.

Sous la direction du :
Directeur de thèse
Gleizes, Marie-Pierre
Hadj Kacem, Ahmed
Migeon, Frédéric
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 ; Unité de Recherche en Développement et Contrôle d’Applications Distribuées (ReDCAD)
Mots-clés libres :Système multi-agents - B-événementiel - Vérification formelle - Temporal logic of actions - Système auto-organisateur - Preuve - Raffinement - Rodin
Sujets :Informatique
Déposé le :09 Feb 2016 14:25