Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Formal Modelling and Verificat...

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

Linas Laibinis, Elena Troubitsyna, Zeineb Graja, Frederic Migeon, Ahmed Hadj Kacem, Formal Modelling and Verification of Cooperative Ant Behaviour in Event-B. In: D. Giannakopoulou, G. Salaun (Eds.), Software Engineering and Formal Methods (SEFM 2014), Lecture Notes in Computer Science 8702, 363–377, Springer, 2014.

http://dx.doi.org/10.1007/978-3-319-10431-7_29

Abstract:

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.

BibTeX entry:

@INPROCEEDINGS{inpLaTrGrMiKa14a,
  title = {Formal Modelling and Verification of Cooperative Ant Behaviour in Event-B},
  booktitle = {Software Engineering and Formal Methods (SEFM 2014)},
  author = {Laibinis, Linas and Troubitsyna, Elena and Graja, Zeineb and Migeon, Frederic and Kacem, Ahmed Hadj},
  volume = {8702},
  series = {Lecture Notes in Computer Science},
  editor = {Giannakopoulou, D. and Salaun, G.},
  publisher = {Springer},
  pages = {363–377},
  year = {2014},
  keywords = {formal modelling, verification, multi-agent systems, cooperative behaviour},
  ISSN = {0302-9743},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB)

Publication Forum rating of this publication: level 1

Edit publication