Authors:
Zeineb Graja
1
;
Frederic Migeon
2
;
Christine Maurel
2
;
Marie-Pierre Gleizes
2
;
Linas Laibinis
3
;
Amira Regayeg
4
and
Ahmed Hadj Kacem
4
Affiliations:
1
University of Sfax and Paul Sabatier University, Tunisia
;
2
Paul Sabatier University, France
;
3
Abo Akademi University, Finland
;
4
University of Sfax, Tunisia
Keyword(s):
Self-organizing MAS, Formal Verification, Design Patterns, Refinement, Event-B.
Related
Ontology
Subjects/Areas/Topics:
Agent Models and Architectures
;
Agents
;
Artificial Intelligence
;
Artificial Intelligence and Decision Support Systems
;
Distributed and Mobile Software Systems
;
Enterprise Information Systems
;
Knowledge Engineering and Ontology Development
;
Knowledge-Based Systems
;
Model-Based Reasoning
;
Multi-Agent Systems
;
Self Organizing Systems
;
Software Engineering
;
Symbolic Systems
Abstract:
Self-Organizing Multi-Agent Systems (SO-MAS) are defined as a set of autonomous entities called agents interacting together in order to achieve a given task. Generally, the development process of these systems is based on the bottom-up approach which focuses on the design of the entities individual behavior. The main question arising when developing SO-MAS is how to insure that the designed entities, when interacting together, will give rise to the desired behavior? Our proposition to deal with this question is to use formal
methods. We propose a correct by construction method for systematic design of SO-MAS based on the use of design patterns and formal stepwise refinements. Our work gives guidelines to assist the designer when developing the individual behavior of the entities and prove its correctness at the early stages of the design process. The method is illustrated with the foraging ants’ case study.