Formal verification of JADE behaviour: A modeling approach

Agent is an autonomous entity who can perform actions to achieve its goal. A multi-agent system (MAS) is a system composed of multiple interacting agents doing activities for a complex system. Since in the real world, MAS have agents acting behaviors concurrently in temporal context, it is hard to completely eliminate failures in such a system. Therefore, a formal verification of a system model is required to ensure the correctness of the MAS design. In this paper, we present the timed trace theoretic verification to detect safety and timing failures in MAS model based on Java Agent Development Framework (JADE), an Application Programming Interface (API) for developing MAS. An example is used to illustrate our proposed method.