Abstract
Multi-Agent paradigm offers a viable solution to the increasing needs for smart and crisis system that reacts accordingly to the environment changes. The researches have largely focused on studying the development of the various approaches that deals with designing and implementing the multi-agent system. However, there is a lack in approaches that treat in depth the specification aspect of the Multi-Agent systems engineering process, which is important to better define and describe the behavior of the agents. This paper is interested in studying the specification and the verification of Multi-Agent behavior, it proposes in consequence an effective method called BECAMEDA. It is based on an iterative process that is useful to understand the system starting from goals identification that the system expects to achieve through the formal verification of the system properties. The method is illustrated by an example of a Crisis Management system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Mattei, S., Bisgambiglia, P.A., Delhom, M., Vittori, E.: Towards discrete event multi agent platform specification. In: Third International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking, pp. 14–21 (2012)
Chuanjun, R., Hongbing, H., Shiyao, J.: Specification of agent in complex adaptive system. In: Computer Science and Computational Technology, ISCSCT 2008, vol. 2, pp. 210–216 (2008)
Sharma, M., Firdaus, M., Chatterjee, R.K., Sarkar, A.: Constraint specification in multi-agent system. In: Region 10 Conference (TENCON), pp. 2404–2409. IEEE (2016)
Subburajand, V.H., Urban, J.E.: Issues and challenges in building a framework for reactive agent systems. In: Complex, Intelligent and Software Intensive Systems (CISIS), pp. 600–605. IEEE (2010)
Bounabat, B., Romadi, R., Labhalla, S.: Designing multiagent reactive systems: a specification method based on reactive decisional agents. In: Pacific Rim International Workshop on Multi-Agents. LNAI, vol. 1733, pp. 197–210. Springer, Heidelberg (1999)
Aaroud, A., Labhalla, S.E., Bounabat, B.: Modelling the handover function of global system for mobile communication. Int. J. Model. Simul. 25(2), 99–105 (2005)
Romadi, R., Berbia, H., Bounabat, B.: Wireless sensor network simulation of the energy consumption by a multi-agents system. J. Theor. Appl. Inf. Technol. 25(1), 50–56 (2011)
Berrada, M.: Qualitative verification of multi-agents reactive decisional system using business process modeling notation. In: Intelligent Agent Technology, pp. 747–751. IEEE (2006)
Kienzle, J., Guelfi, N., Mustafiz, S.: Crisis management systems: a case study for aspect-oriented modeling. In: Transactions on Aspect-Oriented Software Development VII, pp. 1–22. Springer, Heidelberg (2010)
Graja, Z., Migeon, F., Maurel, C., Gleizes, M.P., Kacem, A.H.: A stepwise refinement based development of self-organizing multi-agent systems: application to the foraging ants. In: International Workshop on Engineering Multi-Agent Systems, pp. 40–57. Springer, Heidelberg (2014)
Pereverzeva, I., Troubitsyna, E., Laibinis, L.: Formal development of critical multi-agent systems: a refinement approach. In: Ninth European Dependable Computing Conference, pp. 156–161 (2012)
Chatterjee, R.K., Neha, N., Sarkar, A.: Behavioral modeling of multi agent system: high level petri net based approach. Int. J. Agent Technol. Syst. 7(1), 55–78 (2015)
Hadj-Kacem, A., Regayeg, A., Jmaiel, M.: ForMAAD: a formal method for agent-based application design. Int. J. Web Intell. Agent Syst. 5(4), 435–454 (2007)
Laouadi, M.A., Mokhati, F., Seridi-Bouchelaghem, H.: A novel organizational model for real time mas: towards a formal specification. In: Intelligent Systems for Science and Information, pp. 171–180. Springer International Publishing, Cham (2014)
Haqiq, A., Bounabat, B.: An extended approach for the behavioral and temporal constraints specification of reactive agent. In: 15th International Conference on Intelligent Systems Design and Applications, pp. 329–334. IEEE (2015)
Haqiq, A., Bounabat, B.: UML profile for modeling multi decisional reactive agent system. J. Lect. Notes Softw. Eng. 1(3), 224 (2013). ISSN:2301-3559
Clarke, E.M.: The birth of model checking. In: 25 Years of Model Checking, pp. 1–26. Springer, Heidelberg (2008)
Haqiq, A., Bounabat, B.: Model checking of multi decisional reactive agent system. In: 9th International Conference on Intelligent Systems: Theories and Application, Rabat, Morocco, vol. 1, pp. 133–140 (2014)
Haqiq, A., Bounabat, B.: Verification of multi decisional reactive agent using SMV model checker. In: 8th IEEE International Design and Test Symposium, Marrakesh, Morocco, pp. 1–6 (2013)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an open source tool for symbolic model checking. In: 14th Conference on Computer Aided Verification, LNCS, vol. 2404. Springer, Heidelberg (2002)
Bolotov, A.: A clausal resolution method for CTL branching-time temporal logic. J. Exp. Theor. Artif. Intell. 11(1), 77–93 (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Haqiq, A., Bounabat, B. (2018). BECAMEDA: A Customizable Method to Specify and Verify the Behavior of Multi-agent Systems. In: Ben Ahmed, M., Boudhir, A. (eds) Innovations in Smart Cities and Applications. SCAMS 2017. Lecture Notes in Networks and Systems, vol 37. Springer, Cham. https://doi.org/10.1007/978-3-319-74500-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-74500-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-74499-5
Online ISBN: 978-3-319-74500-8
eBook Packages: EngineeringEngineering (R0)