Vers une modélisation formelle basée sur le raffinement des systèmes multi-agents auto-organisateurs
Résumé
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 as- sume 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.
Le développement de SMA auto-organisateurs manque encore de méthodes rigoureuses de véri¿cation 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éri¿cation 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.