Verification of Multi-Agent Systems (MAS) is vital since it results in reducing design costs. Agent UML (AUML) is a methodology for MAS design that is an extension of Unified Modeling Language (UML). Although UML is used for object-oriented designs, AUML can handle the interactions among agents to deal with agent-based designs. In this thesis, AUML is employed for designing MASs and a set of conversion rules is proposed to convert AUML notations into UML diagrams to be used for MAS verification. Emergent behaviour is a critical problem in MASs that leads to unexpected behaviours due to the assumptions of behaviour model synthesis, i.e. overgeneralization. The main contributions of this thesis are: 1) Designing multi-agent systems using AUML methodology and preparing scenarios for verification. 2) Developing a component-level approach for verifying multi-agent systems preventing overgeneralization. 3) Proposing a system-level algorithm to obtain comprehensive system behaviour analysis.