MAZE: An Extension of Object-Z for Multi-Agent Systems
The formal development of multi-agent systems (MAS) may involve consideration of system functionality at three distinct levels of abstraction. The macro level focusses on the system’s overall, global behaviour, independently of how the agents of the system operate and interact. The meso level focusses on agent interactions, and the micro level on the operation of individual agents. While Object-Z with its high-level support for component-based specifications is well suited to modelling MAS at the macro and meso levels, it can become cumbersome at the micro level where the low-level mechanisms required for dealing with asynchronous communication between agents and timing constraints need to be explicitly defined. In this paper we introduce MAZE, an extension of Object-Z supporting (i) action refinement to facilitate the development process from the macro to micro level, and (ii) a number of syntactic conventions to facilitate micro-level specification. The syntactic conventions are shorthands for existing Object-Z notation and so require no redefinition of Object-Z’s semantics.
KeywordsChange Action MultiAgent System Formal Development Forward Simulation Meso Level
Unable to display preview. Download preview PDF.
- 1.Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press (1986)Google Scholar
- 4.Derrick, J., Boiten, E.: Refinement in Z and Object-Z, Foundations and Advanced Applications, 2nd edn. Springer (2014)Google Scholar
- 5.Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1), 4 (2011)Google Scholar
- 6.Dressler, F.: Self-organization in sensor and actor networks. Wiley (2007)Google Scholar
- 7.Fischer, C.: CSP-OZ - a combination of CSP and Object-Z. In: Bowman, H., Derrick, J. (eds.) FMOODS 1997, pp. 423–438. Chapman & Hall (1997)Google Scholar
- 8.Gerla, M., Kwon, T.J., Pei, G.: On demand routing in large ad hoc wireless networks with passive clustering. In: WCNC 2000, vol. 1, pp. 100–105 (2000)Google Scholar
- 9.Gruer, P., Hilaire, V., Koukam, A., Cetnarowicz, K.: A formal framework for multi-agent systems analysis and design. Expert System Applications 23(4), 349–355 (2002)Google Scholar
- 10.Li, Q., Smith, G.: Using bounded fairness to specify and verify ordered asynchronous multi-agent systems. In: ICECCS 2013, pp. 111–120. IEEE Computer Society Press (2013)Google Scholar
- 11.Smith, G.: The Object-Z Specification Language. Kluwer Academic Publishers (2000)Google Scholar
- 13.Smith, G., Winter, K.: Incremental development of multi-agent systems in Object-Z. In: SEW-35. IEEE Computer Society Press (2012)Google Scholar
- 14.Spivey, J.M.: The Z Notation: a reference manual, 2nd edn. Prentice-Hall (1992)Google Scholar
- 16.Wooldridge, M.: An Introduction to MultiAgent Systems, 2nd edn. Wiley (2009)Google Scholar