Title: Systematic verification of multi-agent systems based on rigorous executable specifications
Author: Holger Giese, Florian Klein
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.
Int. J. of Agent-Oriented Software Engineering, 2007 Vol.1, No.1, pp.28 - 62
Available online: 18 Apr 2007