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: 
zeineb.graja@redcad.org,ahmed.hadjkacem@fsegs.rnu.tn
Page: 
159-183
|
DOI: 
https://doi.org/10.3166/RIA.30.159-183
Received: 
N/A
|
Accepted: 
N/A
|
Published: 
30 April 2016
| Citation
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 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.

Keywords: 

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
  References

Abrial J. (2010). Modeling in Event-B - system and software engineering. Cambridge University Press. Consulté sur http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569

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 http://doi.acm.org/10.1145/1529282.1529747

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 http://dx.doi.org/10.1017/S0269888905000494

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 ftp://ftp.irit.fr/IRIT/SMAC/DOCUMENTS/RAPPORTS/TheseJPGeorge_0704.pdf

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. http://www.springerlink.com/, Springer-Verlag. Consulté sur http://www.springer.com/computer/ai/book/978-3-642-34798-6

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 http://dx.doi.org/10.1504/IJAOSE.2008.017317

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 http://dx.doi.org/10.1007/978-3-642-24559-6_31

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 http://dx.doi.org/10.1016/j.robot.2011.10.005

Lamport L. (1994). The temporal logic of actions. ACM Trans. Program. Lang. Syst., vol. 16, no 3, p. 872–923. Consulté sur http://doi.acm.org/10.1145/177492.177726

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 http://dx.doi.org/10.1007/978-3-642 -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 http://arxiv.org/abs/1210.7035

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 http://dx.doi.org/10.1007/978-3-642-05118-0_18

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 https://hal.archives-ouvertes.fr/hal-00663353

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.