Model Checking of Multi Agent System Architectures Using BigMC
Ahmed Taki Eddine Dib, Zaïdi Sahnoun · Annals of Computer Science and Information Systems · 2015
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.