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 条

[1]

Bakam I., 2000, 1 INT WORKSH FAABS 2

[2]

BARBUCEANU M, 1995, 1 INT C MULT AG SYST, P17

[3]

BARTHELEMY F, 2004, SYSTEMES MULTIAGENTS

[4]

Bellifemine F., 1999, PAAM99. Proceedings of the Fourth International Conference on the Practical Applications of Intelligent Agents and Multi-agent Technology, P97

[5]

Benerecetti M, 2002, LECT NOTES COMPUT SC, V2585, P32

[6]

BENERECETTI M, ELECT P

[7]

BENEVIDES MRF, 2004, ES65304 U FED RIO JA

[8]

Bordini R.H., 2004, LNCS LNAI, V3067, P72, DOI [10.1007/978-3- 540- 25936-7 4, DOI 10.1007/978-3-540-25936-74]

[9]

Bordini RH, 2003, LECT NOTES COMPUT SC, V2725, P110

[10]

Boudiaf N, 2005, LECT NOTES ARTIF INT, V3371, P29

← 1 2 3 4 5 →