Translating AUML Diagrams into Maude Specifications: A Formal Verification of Agents Interaction Protocols.
Farid Mokhati, Noura Boudiaf, Mourad Badri, Linda N. Badri · The Journal of Object Technology · 2007
Agents Interaction Protocols (AIPs) play a crucial role in multi-agents systems development.They allow specifying sequences of messages between agents.Major proposed protocols suffer from many weaknesses.We present, in this paper, a formal approach supporting the verification of agents' interaction protocols described by using AUML formalism.The considered AUML diagrams are formally translated into Maude specifications.Based on rewriting logic, the formal and object-oriented language Maude offers an interesting way for concurrent systems formal specification and programming.The Maude environment integrates a model-checker based on Linear Temporal Logic (LTL) supporting formal verification of distributed systems.The proposed approach essentially allows: (1) translating the description of agents' interactions, specified using AUML formalism, in a Maude specification and, (2) applying the model-checking techniques supported by Maude to verify some properties of the described system.A case study is presented to illustrate our approach.