Verification of JADE Agents Using ATL Model Checking

It is widely accepted that the key to successfully developing a system is to produce a thorough system specification and design. This task requires an appropriate formal method and a suitable tool to determine whether or not an implementation conforms to the specifications. In this paper we present an advanced technique to analyse, design and debug JADE software agents, using Alternating-time Temporal Logic (ATL) which is interpreted over concurrent game structures, considered as natural models for compositions of open systems. In development of the proposed solution, we will use our original ATL model checker. In contrast to previous approaches, our tool permits an interactive or programmatic design of the ATL models as state-transition graphs, and is based on client/server architecture: ATL Designer, the client tool, allows an interactive construction of the concurrent game structures as a directed multi-graphs and the An Checker, the core of our tool, represents the server part and is published as Web service.