Formal development of multi-agent systems using MAZE

MAZE is an extension of the Object-Z specification language supporting the specification and development of multi-agent systems (MAS). Following recommendations from the agent-oriented software engineering community, it supports three distinct levels of abstraction: (i) the macro level which focusses on the system's overall, global behaviour, independently of how the agents of the system operate and interact, (ii) the meso level which focusses on agent interactions, and (iii) the micro level which focusses on the operation of individual agents. Object-Z's high-level support for component-based specification, which is well suited to modelling MAS, is complemented in MAZE with support for action refinement to facilitate the top-down development process from the macro to micro level, and with a number of syntactic conventions aimed at abstractly specifying the low-level mechanisms required for dealing with asynchronous communication and timing constraints at the micro level. The latter are shorthands for existing Object-Z notation and so require no redefinition of Object-Z's semantics. In this paper, we provide an overview of MAZE and illustrate its use on a non-trivial case study: a swarm robotic algorithm for self-assembly.