Περίληψη:
Formal development of agent systems with inherent high complexity is not a trivial task, especially if a formal method used is not accompanied by an appropriate methodology. X-machines is a formal method that resembles Finite State Machines but has two important extensions, namely internal memory structure and functions. In this paper, we present a disciplined methodology for developing agent systems using communicating X-machine agents and we demonstrate its applicability through an example. In practice, the development of a communicating system model can be based on a number of well-defined distinct steps, i.e. development of types of X-machine models, agents as instances of those types, communication between agents, and testing as well as model checking each of these agents individually. To each of the steps a set of appropriate tools is employed. Therefore the proposed methodology utilises a priori techniques to avoid any flaws in the early stages of the development together with a posteriori techniques to discover any undiscovered flaws in later stages. This way it makes the best use of the development effort to achieve highest confidence in the quality of the developed agents. We use this methodology for modelling naturally distributed systems, such as multi-agent systems. We use a generalized example in order to demonstrate the methodology and explain in detail how each activity is carried out. We briefly present the theory behind communicating X-machine agents and then we describe in detail the practical issues related using the same example throughout.