Vers une modélisation formelle basée sur le raffinement des systèmes multi-agents auto-organisateurs

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érifications 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 robustesse. 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.