OPEN ACCESS
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.
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.