Paper Info
Title
Model checking of Multi Agent System architectures using BigMC
Abstract
Formal methods offer a great potential for early integration of verification in the design process. These are based on theories and mathematical notations that allow the formal specification of a program and check its implementation. They offer a global vision and a high-level structure and system organization. In addition, the software architecture plays a key role as a pivot point between the requirements of a system and its implementation. In this paper, we present a formal approach based on Bigraphical Reactive Systems for specifying and verifying the main features of the Multi Agent Systems (MAS) architectures based on the Belief-Desire-Intention (BDI) agent model. The proposed approach supports both the static and dynamic aspects of BDI-MAS architectures at different levels of abstraction. Further, we use automatic proof tool BigMc to analyze the specifications and verify system properties.
Year
DOI
Venue
2015
10.15439/2015F300
FedCSIS
Keywords
DocType
Volume
Multi-Agent Systems,software architecture description language,Bigraphical Reactive System,formal specification,reconfiguration,formal verification,Bigraphical Model Checker
Conference
5
ISSN
Citations 
PageRank 
2300-5963
0
0.34
References 
Authors
14
2
Name
Order
Citations
PageRank
Ahmed Taki Eddine Dib101.01
Zaïdi Sahnoun2269.08