A Maude-Based Tool for Simulating DIMA Model

Conference paper
Part of the Lecture Notes in Electrical Engineering book series (LNEE, volume 27)


The lack of formal semantics in the existing formalisms describing multi-agents models, combined with the complexity of multi-agents systems, are sources of several problems during their development process. The formal methods are known to bring rigorous and precise descriptions. They offer the possibility of checking the correction of specifications. In this framework and in previous papers (Ferber J, Gutknecht O (2002) MadKit user’s guide. Version 3.1) [23], we have proposed a formal and generic framework called DIMA-Maude, allowing formal description and validation of the DIMA model [15] with the Maude language [22]. This language, based on rewriting logic [21], offers a rich notation supporting formal specification, implementation, validation through simulation, and verification through accessibility analysis and model checking of concurrent systems (Koning JL (1999) Algorithms for translating interaction protocols into a formal description. In: IEEE Int Conf Syst Man Cybernet Conf, Tokyo, Japan). In this paper, we propose a rewriting logic-based tool for creating a DIMA model. This tool allows the edition and the simulation of a DIMA system. It allows the user to draw a DIMA system graphically and translates the graphical representation of the drawn DIMA model to a Maude specification. Then the Maude system is used to perform the simulation of the resulting Maude specification. This tool allows preserving the graphic notations offered by the DIMA model for clarity and getting a formal specification in Maude for analysis.


Model Check Functional Module Concurrent System Method IsAlive Proactive Agent 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    AgentBuilder RM (2000). An integrated toolkit for constructing intelligent software agents. Reference ManualGoogle Scholar
  2. 2.
    Bakam I, Kordon F, Le Page C, Bousquet F (2000) Formalization of a spatialized multiagent model using coloured Petri nets for the study of a hunting management system. In: FAABS2000, GreenbeltGoogle Scholar
  3. 3.
    Boudiaf N, Mokhati F, Badri M, Badri L (2005) Specifying DIMA multi-agent models using Maude. Springer-Verlag, Berlin, Heideberg LNAI 3371:29–42Google Scholar
  4. 4.
    Clavel M et al. (2005) Maude manual (Version 2.2). Internal report, SRI InternationalGoogle Scholar
  5. 5.
    DeLoach SA, Wood M (2001) Developing multiagent systems with agent tool. In: ATAL’2000, BerlinGoogle Scholar
  6. 6.
    Ferber J, Gutknecht O (2002) MadKit user’s guide. Version 3.1Google Scholar
  7. 7.
    Guessoum Z (2003) Modèles et architéctures d’agents et de systèmes multi-agents adaptatifs. Dossier d’habilitation à diriger des recherches de l’Université Pierre et Marie CurieGoogle Scholar
  8. 8.
    Koning JL (1999) Algorithms for translating interaction protocols into a formal description. In: IEEE International conference on systems, man, and cybernetics. Tokyo, JapanGoogle Scholar
  9. 9.
    Meseguer J (1996) Rewriting logic as a unified model of concurrency: a progress report. Springer-Verlag LNCS 119:331–372Google Scholar
  10. 10.
    Meseguer J (2000) Rewriting logic and Maude: a wide-spectrum semantic framework for object-based distributed systems. In: FMOODS2000Google Scholar
  11. 11.
    Mokhati F, Boudiaf N, Badri M, Badri L (2004) DIMA-Maude: Toward a formal framework for specifying and validating DIMA agents. In: Proceedings of Moca’04, Aarhus, DenmarkGoogle Scholar
  12. 12.
    Mokhati F, Boudiaf N, Badri M, Badri L (2007) Translating AUML diagrams into Maude specifications: a formal verification of agents interaction protocols. J Obj Technol, ISSN 1660–1769, USAGoogle Scholar
  13. 13.
    Torroni P (2004) Computational logic in multi-agent systems: recent advances and future directions, computational logic in multi-agent systems. Ann Math Artif Intell 42(1–3):293–305CrossRefMATHGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2009

Authors and Affiliations

  1. 1.Computer Science DepartmentUniversity of Oum El BouaghiAlgeria

Personalised recommendations