Affiliations: Laboratory MIRACL, Faculté des Sciences
Économiques et de Gestion de Sfax, Tunisia | Laboratory ReDCAD, École Nationale d'Ingénieurs
de Sfax, Tunisia
Note: [] Corresponding author: Ahmed Hadj-Kacem, Laboratory MIRACL,
Faculté des Sciences Économiques et de Gestion de Sfax B.P.1088, 3018
Sfax, Tunisia. Tel.: +216 74 27 87 77; Fax: +216 74 27 91 39; E-mail:
[email protected]
Abstract: This paper has two purposes. First, it defines a formal language,
for specifying agent-based applications, that integrates linear temporal logic
to the Z notation. This integration offers a language that is expressive enough
to cover both individual agent aspects (e.g., knowledge, goals and roles) as
well as collective aspects (e.g., cooperation strategy, organization structure
and collective behaviour). Second, it proposes a formal methodology for
designing agent-based applications using stepwise refinements. The main
contribution of our design process consists of a set of methodological
principles and hints that help the user to build, in a systematic and
incremental way, a verified design starting from abstract requirements. This
approach will be illustrated by developing an agent-based solution for the air
traffic control problem.
