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
相关论文
共 50 条
  • [31] Formal Verification for Node-Based Visual Scripts Using Symbolic Model Checking
    Hasegawa, Isamu
    Yokogawa, Tomoyuki
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2022, E105D (01) : 78 - 91
  • [32] A formal approach for the modelling and verification of multiagent plans based on model checking and Petri nets
    de Almeida, HO
    da Silva, LD
    Perkusich, A
    Casto, ED
    SOFTWARE ENGINEERING FOR MULTI-AGENT SYSTEMS III: RESEARCH ISSUES AND PRACTICAL APPLICATIONS, 2004, 3390 : 162 - 179
  • [33] Formal verification of dynamic hybrid systems: a NuSMV-based model checking approach
    Xu, Zhi
    Zhong, Deming
    Li, Weigang
    Huang, Hao
    Sun, Yigang
    4TH ANNUAL INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATION AND SENSOR NETWORK (WCSN 2017), 2018, 17
  • [34] A Formal Approach for Modeling and Verification of Bus Bridge Based on Petri Net and Model Checking
    Zhang, Guoyin
    Liu, Ming
    Yao, Aihong
    PROCEEDINGS 2010 3RD IEEE INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGY, (ICCSIT 2010), VOL 1, 2010, : 335 - 339
  • [35] Abstraction Framework and Complexity of Model Checking Based on the Promela Models
    Chen Daoxi
    Zhang Guangquan
    Fan Jianxi
    ICCSSE 2009: PROCEEDINGS OF 2009 4TH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE & EDUCATION, 2009, : 857 - 861
  • [36] Design Model of Multi-Agents Based Autonomous Railway Vehicles Control System
    Khan, M. Saleem
    Benkrid, Khaled
    IMECS 2009: INTERNATIONAL MULTI-CONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, VOLS I AND II, 2009, : 1260 - +
  • [37] Formal Verification of Autonomous Vehicles: Bridging the Gap between Model-Based Design and Model Checking
    Rao A.
    Wang Y.
    SAE International Journal of Advances and Current Practices in Mobility, 2023, 6 (02): : 814 - 826
  • [38] A Study on Trust of E-commerce Market Based on Multi-agents Model
    Wu Chuan-Zhen
    Liu Yun-Ping
    Xu Di
    ELEVENTH WUHAN INTERNATIONAL CONFERENCE ON E-BUSINESS, 2012, : 144 - 155
  • [39] Research on the model of ontology-based knowledge sharing for multi-agents system
    Zhao, Tian-Xiao Tan Hui
    Zhao, Zong-Tao
    Information, Management and Algorithms, Vol II, 2007, : 257 - 259
  • [40] RESEARCH AND APPLICATION OF MULTI-AGENTS MODEL IN CSCW-BASED CAD SYSTEM
    Xu Hui-Fang
    Shi Wei-Feng
    FIFTH INTERNATIONAL CONFERENCE ON ADVANCED COMPUTER THEORY AND ENGINEERING (ICACTE 2012), 2012, : 73 - 77
12345