ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique

APPEL À
CONTRIBUTION
Masses de données hétérogènes
En savoir plus >>
Autres revues >>

Revue d'Intelligence Artificielle

0992-499X
Revue des Sciences et Technologies de l'Information
 

 ARTICLE VOL 30/1-2 - 2016  - pp.159-183  - doi:10.3166/ria.30.159-183
TITRE
Vers une modélisation formelle basée sur le raffinement des systèmes multi-agents auto-organisateurs

TITLE
Towards a formal modelling based refinement of self-organizing multi-agent systems

RÉSUMÉ
Le développement de SMA auto-organisateurs manque encore de méthodes rigoureuses de vérification garantissant la robustesse et la résilience du système conçu. De telles assurances peuvent être obtenues grâce à l’application de méthodes formelles. Mais l’intégration de ces techniques de vérification reste encore modeste due à la complexité liée à la dynamique des SMA auto-organisateurs qui fait émerger leur fonction globale. Dans cet article, nous explorons le potentiel des langages formels, en particulier B-événementiel et la logique TLA, pour prouver des propriétés liées à la convergence et la résilience. Nous supposons que ces propriétés pourront d’abord être observées au niveau global par simulation. Les techniques formelles nous permettront ensuite d’en faire la preuve. Notre travail est illustré par l’étude de cas des fourmis fourrageuses.


ABSTRACT
The development of self-organizing MAS still lacks rigorous verification methods to ensure the convergence and resilience of the designed system. Such insurances can be obtained through the application of formal methods. However, the integration of these techniques is still modest due to the complexity of the dynamics of self-organizing MAS which makes the overall function emerging. In this article, we explore the potential of formal languages, in particular Event-B and the TLA logic to prove the convergence and the resilience of the system. We assume that these properties can first, be observed at the global level by simulation. Then, Formal techniques allow us to prove them. Our work is illustrated by the foraging ant’s case study.


AUTEUR(S)
Zeineb GRAJA, Frédéric MIGEON, Christine MAUREL, Marie-Pierre GLEIZES, Ahmed HADJ KACEM

MOTS-CLÉS
SMA auto-organisateurs, fourmis fourrageuses, vérification formelle, B-événementiel, TLA.

KEYWORDS
self-organizing MAS, foraging ants, formal verification, Event-B, TLA.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (268 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier