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

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

Zeineb Graja
Frédéric Migeon
Christine Maurel
Marie-Pierre Gleizes
Ahmed Hadj Kacem

Unité de Recherche en Développement et Contrôle d’Applications Distribuées, Faculté des Sciences Economiques et de Gestion - Université de Sfax, Tunisie

Unité de Recherche en Développement et Contrôle d’Applications Distribuées, Faculté des Sciences Economiques et de Gestion - Université de Sfax, Tunisie

Corresponding Author Email:,
30 April 2016
| Citation

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.


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

1. Introduction
2. Travaux antérieurs
3. Modélisation formelle d’un SMA auto-organisateur
4. Application aux fourmis fourrageuses
5. Conclusion et perspectives

Abrial J. (2010). Modeling in Event-B - system and software engineering. Cambridge University Press. Consulté sur

Casadei M., Viroli M. (2009). Using probabilistic model checking and simulation for designing self-organizing systems. In Proceedings of the 2009 acm symposium on applied computing, p. 2103–2104. New York, NY, USA, ACM. Consulté sur

Di Marzo Serugendo G., Gleizes M.-P., Karageorgos A. (2005, juin). Self-organization in multiagent systems. In Knowl. eng. rev., vol. 20, p. 165–189.

New York, NY, USA, Cambridge University Press. Consulté sur

Gardelli L., Viroli M., Omicini A. (2006). Exploring the dynamics of self-organising systems with stochastic -calculus: Detecting abnormal behaviour in MAS. In In mas. in: Fifth international symposium from agent theory to agent implementation (at2ai5.

Georgé J.-P. (2004). Résolution de problèmes par à c mergence, Etude d’un Environnement de Programmation émergente. Thèse de doctorat, Université Paul Sabatier, Toulouse, France. Consulté sur

Gleizes M.-P. (2012). Self-adaptive Complex Systems (regular paper). In M. Cossentino, M. Kaisers, K. Tuyls, G. Weiss (Eds.), European Workshop on Multi-Agent Systems (EUMAS), Maastricht, The Netherlands, 13/11/2011-16/11/2011, vol. 7541, p. 114–128., Springer-Verlag. Consulté sur

Hilaire V., Gruer P., Koukam A., Simonin O. (2008). Formal driven prototyping approach for multiagent systems. IJAOSE, vol. 2, no 2, p. 246–266. Consulté sur

Hoang T. S., Abrial J. (2011). Reasoning about liveness properties in Event-B. In Formal methods and software engineering - 13th international conference on formal engineering methods, ICFEM 2011, durham, uk, october 26-28, 2011. proceedings, p. 456–471. Consulté sur

Konur S., Dixon C., Fisher M. (2012, février). Analysing robot swarm behaviour via probabilistic model checking. Robot. Auton. Syst., vol. 60, no 2, p. 199–213. Consulté sur

Lamport L. (1994). The temporal logic of actions. ACM Trans. Program. Lang. Syst., vol. 16, no 3, p. 872–923. Consulté sur

Méry D., Poppleton M. (2013). Formal modelling and verification of population protocols. In Integrated formal methods, 10th international conference, IFM 2013, turku, finland, june 10-14, 2013. proceedings, p. 208–222. Consulté sur -38613-8_15

Pereverzeva I., Troubitsyna E., Laibinis L. (2012). Development of fault tolerant MAS with cooperative error recovery by refinement in Event-B. CoRR, vol. abs/1210.7035. Consulté sur

Serugendo G. D. M. (2009). Robustness and dependability of self-organizing systems - A safety engineering perspective. In Stabilization, safety, and security of distributed systems, 11th international symposium, SSS 2009, lyon, france, november 3-6, 2009. proceedings, p.254–268. Consulté sur

Simonin O., Lanoix A., Scheuer A., Charpillet F. (2011, novembre). Specifying in B the Influence/Reaction Model to Study Situated MAS: Application to vehicles platooning. In V2CS : First International workshop on Verification and Validation of multi-agent models for complex systems, p. 15 pages. France. Consulté sur

Topin X., Régis C., Gleizes M.-P., Glize P. (1999, octobre). Comportements individuels adaptatifs dans un environnement dynamique pour l’exploitation collective de ressources . In Intelligence Artificielle Située, cerveau, corps et environnement (IAS’99), Paris, France, 25/10/1999-26/10/1999. Hermès.