Translating AUML Diagrams into Maude Specifications: A Formal Verification of Agents Interaction Protocols

被引：2
|
作者：
Mokhati, Farid [1 ]
Boudiaf, Noura [2 ]
Badri, Mourad [3 ]
Badri, Linda [3 ]
机构：
[1] Univ Larbi Ben Mhidi, Dept Informat, Oum El Bouaghi, Algeria
[2] CNAM, Lab Ceder, Paris, France
[3] Univ Quebec Trois Rivieres, Dept Math & Informat, Trois Rivieres, PQ, Canada
来源：
JOURNAL OF OBJECT TECHNOLOGY | 2007年 / 6卷 / 04期
关键词：
D O I：
10.5381/jot.2007.6.4.a2
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：77 / 102
页数：26
相关论文
共 14 条
  • [1] Generating Maude formal specifications from AUML diagrams
    Mokhati, Farid
    Boudiaf, Noura
    Badri, Linda
    Badri, Mourad
    JOURNAL OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING, 2006, 6 (5-6) : S73 - S89
  • [2] Automated testing sequences generation from AUML diagrams: A formal verification of agents' interaction protocols
    Department of Computer Science, University of Oum El-Bouaghi, Oum El-Bouaghi, Algeria
    不详
    不详
    Int. J. Agent-Oriented Softw. Eng., 2008, 4 (422-448):
  • [3] Formal semantics for AUML agent interaction protocol diagrams
    Cabac, L
    Moldt, D
    AGENT-ORIENTED SOFTWARE ENGINEERING V, 2005, 3382 : 47 - 61
  • [4] Rules for translating interaction protocols into a B formal representation
    Fadil, H
    Koning, JL
    2005 IEEE/WIC/ACM INTERNATIONAL CONFERENCE ON INTELLIGENT AGENT TECHNOLOGY, PROCEEDINGS, 2005, : 495 - 498
  • [5] Formal description and verification of MAS interaction protocols
    Chen, Hongbing
    Yang, Qun
    Li, Qianmu
    Xu, Manwu
    MULTIAGENT AND GRID SYSTEMS, 2006, 2 (04) : 353 - 363
  • [6] A Graph Transformation Approach to Generate Analysable Maude Specifications from UML Interaction Overview Diagrams
    Djaoui, Chafika
    Kerkouche, Elhillali
    Khalfaoui, Khaled
    Chaoui, Allaoua
    2018 IEEE INTERNATIONAL CONFERENCE ON INFORMATION REUSE AND INTEGRATION (IRI), 2018, : 511 - 517
  • [7] Formal consistency verification of deliberative agents with respect to communication protocols
    Ramírez, J
    de Antonio, A
    FORMAL APPROACHES TO AGENT-BASED SYSTEMS, 2005, 3228 : 222 - 237
  • [8] Generating Maude Specifications from UML Interaction Overview Diagrams: A Graph Transformation Based Approach
    Djaoui, Chafika
    Kerkouche, Elhillali
    Chaoui, Allaoua
    Khalfaoui, Khaled
    2018 FIFTH INTERNATIONAL SYMPOSIUM ON INNOVATION IN INFORMATION AND COMMUNICATION TECHNOLOGY (ISIICT 2018), 2018, : 109 - 116
  • [9] Specification and verification of multi-agent systems interaction protocols using a combination of AUML and Event B
    Ben Ayed, Leila Jemni
    Siala, Fatma
    INTERACTIVE SYSTEMS: DESIGN, SPECIFICATION, AND VERIFICATION, PROCEEDINGS, 2008, 5136 : 102 - 107
  • [10] Formal verification of Condition Data Flow Diagrams for assurance of correct network protocols
    Liu, SY
    AINA 2003: 17TH INTERNATIONAL CONFERENCE ON ADVANCED INFORMATION NETWORKING AND APPLICATIONS, 2003, : 289 - 292
12