Today, the agent-oriented methodologies become increasingly attractive to the software system development industry. These methodologies mostly use object-oriented paradigms by concepts like autonomy, pro activity, reactivity, cooperation and alike. There are different agent-oriented methodologies each with different phases and diagrams. However, most of them are using informal graphical diagrams. Hence, automatic analysis of these diagrams may be a challenge. Automated analysis capabilities are necessary to develop high quality software systems. To alleviate this problem, using a formal method to describe the underlying semantics seems necessary. Since graph transformation systems (GTS) are widely used for defining the syntax and semantics of different diagrams and notations formally, in this paper, we are using GTS to formalize agent-oriented methodologies. Among different agent-oriented methodologies, we consider Tropos, because it is basically agent-based, in contrast to the other methodologies which are extensions of the existing object-oriented methodologies. To do so, our proposal consists of four steps: first, we define a meta-model for the abstract syntax of the existing diagrams which are used by the methodology (as a type graph); second, the structural diagrams are defined using host graphs consistent with the designed meta-model and behavioral ones using graph rules. Third, we refine the diagrams automatically to generate some detailed diagrams along with the JACK skeleton codes, and four, we finally verify and validate all the steps through checking consistency, compatibility, correctness and so on.
