Title: Systematic verification of multi-agent systems based on rigorous executable specifications

Authors: Holger Giese, Florian Klein

Addresses: Software Engineering Group, University of Paderborn, Warburger Str. 100, D-33098 Paderborn, Germany. ' Software Engineering Group, University of Paderborn, Warburger Str. 100, D-33098 Paderborn, Germany

Abstract: The multi-agent paradigm provides abstractions that facilitate the design of complex systems consisting of heterogeneous, autonomous components. Most methodologies focus on the specification of complex agent interactions using the social system metaphor, while the interaction between agents and their environment has only recently started to receive more attention. In this paper, we present an approach for making complex Multi-Agent System (MAS) specifications including a detailed environment model amenable to verification. We introduce a formalisation for executable specifications of social systems, which we subsequently use to support their systematic verification by means of simulation and formal verification. We explore which results may be obtained for the overall system and where compositional techniques can be used to separate the specification into more manageable subsets. A case study is used throughout the paper to illustrate the concepts and present results of our verification experiments.

Keywords: multi-agent systems; MAS; executable specifications; formal verification; simulation; model checking; agents; agent-oriented software engineering; agent-based systems.

DOI: 10.1504/IJAOSE.2007.013264

International Journal of Agent-Oriented Software Engineering, 2007 Vol.1 No.1, pp.28 - 62

Published online: 18 Apr 2007 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article