Formal verification of self-adaptive multi-agent systems

Vérification formelle des systèmes multi-agents auto-adaptatifs

Zeineb Graja (1, 2)

1 IRIT-SMAC - Systèmes Multi-Agents Coopératifs
2 REDCAD - Unité de Recherche en développement et contrôle d'applications distribuées

A major challenge for the development of self-organizing MAS is to guarantee the convergence of the system to the overall function expected by an external observer and to ensure that agents are able to adapt to changes. In the literature, several works were based on simulation and model-checking to study self-organizing MAS. The simulation allows designers to experiment various settings and create some heuristics to facilitate the system design. Model checking provides support to discover deadlocks and properties violations. However, to cope with the complexity of self-organizing MAS, the designer also needs techniques that support not only verification, but also the development process itself. Moreover, such techniques should support disciplined development and facilitate reasoning about various aspects of the system behavior at different levels of abstraction. In this thesis, three essential contributions were made in the field of formal development and verification of self-organizing MAS: a formalization with the Event-B language of self-organizing MAS key concepts into three levels of abstraction, an experimentation of a top-down refinement strategy for the development of self-organizing MAS and the definition of a bottom-up refinement process based on refinement patterns.

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.

Mots clés: Self organizing systems; Proof; Formal verification; Multi-agent systems; Refinement; Event-B

Mots clés: Rodin; Système multi-agents; B-événementiel; Vérification formelle; Temporal logic of actions; Système auto-organisateur; Preuve; Raffinement

Domaines: Système multi-agents [cs.MA]

Zeineb Graja. Vérification formelle des systèmes multi-agents auto-adaptatifs. Système multi-agents [cs.MA]. Université Paul Sabatier - Toulouse III, 2015. Français. ⟨NNT : 2015TOU30105⟩. ⟨tel-01320778⟩