SUPPORTING FORMAL VERIFICATION OF DIMA MULTI-AGENTS MODELS: TOWARDS FRAMEWORK BASED ON MAUDE MODEL CHECKING

被引：6
作者：
Boudiaf, Noura [1 ]
Mokhati, Farid [1 ]
Badri, Mourad
机构：
[1] Univ Oum El Bouaghi, Dept Comp Sci, Oum El Bouaghi, Algeria
来源：
INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING | 2008年 / 18卷 / 07期
关键词：
Multi-agents systems; quality assurance; DIMA model; formal specification; rewriting logic; Maude; behavior; verification; model checking;
D O I：
10.1142/S021819400800391X
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Model Checking based verification techniques represent an important issue in the field of concurrent systems quality assurance. The lack of formal semantics in the existing formalisms describing multi-agents models combined with multi-agents systems complexity are sources of several problems during their development process. The Maude language, based on rewriting logic, offers a rich notation supporting formal specification and implementation of concurrent systems. In addition to its modeling capacity, the Maude environment integrates a Model Checker based on Linear Temporal Logic (LTL) for distributed systems verification. In this paper, we present a formal and generic framework (DIMA-Maude) supporting formal description and verification of DIMA multi-agents mode.
引用
收藏
页码：853 / 875
页数：23
相关论文
共 45 条
[41]   Computational logic in multi-agent systems: Recent advances and future directions [J].
Torroni, P .
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2004, 42 (1-3) :293-305
[42]  
TORRONI P, 2004, ELECT NOTES THEORETI, V70
[43]  
Verdejo A., 2000, Formal Methods for Distributed System Development. FORTE/PSTV 2000. IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX), P351
[44]  
WOOLDRIDGE M, 2002, P 1 INT JOINT C AU 2
[45]  
Wooldridge M.J., 1995, KNOWLEDGE ENG REV, V10
12345