Formal Modelling and Verification of Cooperative Ant Behaviour in Event-B

详细信息    查看全文

• 作者：Linas Laibinis (17)
  Elena Troubitsyna (17)
  Zeineb Graja (18) (19)
  Frédéric Migeon (19)
  Ahmed Hadj Kacem (18)
  
• 关键词：Self ; organizing MAS ; cooperative ants ; formal verification ; refinement ; Event ; B
• 刊名：Lecture Notes in Computer Science
• 出版年：2014
• 出版时间：2014
• 年：2014
• 卷：8702
• 期：1
• 页码：363-377
• 全文大小：258 KB
• 参考文献：1. Abrial, J.-R.: Modelling in Event-B. Cambridge University Press (2010)
  2. Bonjean, N., Mefteh, W., Gleizes, M.-P., Maurel, C., Migeon, F.: ADELFE 2.0. In: Handbook on Agent-Oriented Design Processes. Springer
  3. Camps, V.: Vers une théorie de l’auto-organisation dans les systèmes multi-agents basée sur la coopération: application à la recherche d’information dans un système d’information répartie. PhD thesis, Paul Sabatier university (1998)
  4. Capera, D., Georgé, J.-P., Gleizes, M.P., Glize, P.: The AMAS theory for complex problem solving based on self-organizing cooperative agents. In: WETICE, pp. 383-88 (2003)
  5. Casadei, M., Viroli, M.: Using probabilistic model checking and simulation for designing self-organizing systems. In: Proceedings of the 2009 ACM Symposium on Applied Computing, pp. 2103-104. ACM, New York (2009) CrossRef
  6. Di Marzo Serugendo, G., Gleizes, M.-P., Karageorgos, A. (eds.): Self-organising Software - From Natural to Artificial Adaptation. Natural Computing Series. Springer (October 2011), http://www.springerlink.com
  7. Gardelli, L., Viroli, M., Omicini, A.: Exploring the Dynamics of Self-Organising Systems with Stochastic / π-Calculus: Detecting Abnormal Behaviour in MAS. In: Trappl, R. (ed.) Proceedings of 18th European Meeting on Cybernetics and Systems Research (EMCSR 2006), Vienna, Austria, vol.?2, pp. 539-44 (2006)
  8. Gleizes, M.-P., Camps, V., Georgé, J.-P., Capera, D.: Engineering systems which generate emergent functionalities. In: Weyns, D., Brueckner, S.A., Demazeau, Y. (eds.) EEMMAS 2007. LNCS (LNAI), vol.?5049, pp. 58-5. Springer, Heidelberg (2008) CrossRef
  9. Hallerstede, S., Hoang, T.S.: Qualitative Probabilistic Modelling in Event-B. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.?4591, pp. 293-12. Springer, Heidelberg (2007) CrossRef
  10. Konur, S., Clare, D., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robot. Auton. Syst.?60(2), 199-13 (2012) CrossRef
  11. Laibinis, L., Troubitsyna, E.: Refinement of Fault Tolerant Control Systems in B. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol.?3219, pp. 254-68. Springer, Heidelberg (2004) CrossRef
  12. Pereverzeva, I., Troubitsyna, E., Laibinis, L.: Formal Development of Critical Multi-agent Systems: A Refinement Approach. In: EDCC, pp. 156-61 (2012)
  13. Rodin platform. Automated tool environment for Event-B, http://rodin-b-sharp.sourceforge.net/
  
• 作者单位：Linas Laibinis (17)
  Elena Troubitsyna (17)
  Zeineb Graja (18) (19)
  Frédéric Migeon (19)
  Ahmed Hadj Kacem (18)
  
  17. ?bo Akademi University, Turku, Finland
  18. Research Laboratory on Development and Control of Distributed Applications (ReDCAD), Faculty of Economics and Management, University of Sfax, Tunisia
  19. Institute for Research in computer Science in Toulouse (IRIT), Paul Sabatier University, Toulouse, France
  
• ISSN：1611-3349

文摘

Multi-agent technology is a promising approach to development of complex decentralised systems that dynamically adapt to changing environmental conditions. The main challenge while designing such multi-agent systems is to ensure that reachability of the system-level goals emerges through collaboration of autonomous agents despite changing operating conditions. In this paper, we present a case study in formal modelling and verification of a colony of foraging ants. We formalise the behaviour of cooperative ants in Event-B and verify by proofs that the desired system-level properties become achievable via agent collaboration. The applied refinement-based approach weaves proof-based verification into the formal development. It allows us to rigorously define constraints on the environment and the ant behaviour at different abstraction levels and systematically explore the relationships between system-level goals, environment and autonomous ants. We believe that the proposed approach helps to structure complex system requirements, facilitates formal analysis of various system interdependencies, and supports formalisation of intricate mechanisms of agent collaboration.