Agent oriented development (AOD) is a promising approach for designing complex software systems which constitute now a part of the infrastructure of the modern society.

The AOD approach was applied in the development of several industrial applications in various fields, such as distributed network management and intelligent WEB services. The strength of this approach in solving complex problems stems from the fact that agents, thanks to their autonomy and adaptability, are able to achieve their goals in a rather flexible way, while interacting with each other through high level language concepts and protocols. However, this flexibility in solving problems reveals difficulties when designing agents and agent societies. Indeed, developers have to deal with new concepts related to two levels: (1) agent individual aspects such as autonomy, goal, knowledge, capability and role; and (2) phenomena resulting from collective and social aspects, such as organization, cooperation, negotiation and coordination.

Our approach for dealing with the inherent complexity of agent-based application development, called ForMAAD (Formal Method for Agent-based Application Design), is based on two complementary principles of software formal design. The first principle stresses the need of a formal specification that describes the system requirements in an abstract way. This specification allows to perform rigorous reasoning about the desired properties. The second principle emphasizes a formal methodology to systematically construct a correct (verified) design specification. Following these principles, first, we propose an agent-oriented formal specification language that covers individual (static and behavioural) aspects of agents (e.g., knowledge, goal, and role) as well as collective aspects of multi-agent applications (e.g., collective behaviour and organization structure).

This language integrates linear temporal logic into the Z notation. The integration was motivated by recent tendencies to (1) address aspects separately using suitable languages and tools; and (2) integrate various approaches in a unified development process.

Indeed, the Z language possesses all necessary features for handling structural and functional aspects of agents (e.g., the mental state and associated treatments), whereas the linear temporal logic is considered as one of the most eminent formalisms for specifying reactive behaviours of agents. In order to provide a formal interpretation of the defined temporal operators, we developed an operational semantics for agent-based applications in terms of sequences of system states. The definition of this temporal model within the Z notation enable us to use tools supporting raw Z notation, such as Z/EVES, for verification purposes. Such tools allowed us to perform syntax, type, and domain checking of our specifications and to reason about correctness by proving several properties.

To assist a designer in specifying an agent-based application using our language, we define an agent-based design methodology based on stepwise refinements. More specifically, we provide a set of refinement steps to generate, step by step, individual agent behaviours starting from an abstract specification. Furthermore, we propose guidelines that help (1) to define a cooperation strategy for achieving the given common goal, (2) to set an appropriate organization structure, then (3) to identify the needed communication actions, and finally, (4) to derive the intended agents behaviours. In order to guarantee the correctness of the design specification, we have formulated, for each refinement step, an appropriate proof obligation. This latter ensures that the refined specification preserves the properties of the application to develop. Concretely, proof obligations show that the designed agents are able to achieve the initially specified common goal.