Rigorous Development of Fault-Tolerant Agent Systems

Agent systems are examples of complex distributed systems. Though agents operate in unreliable communication environment, often such systems have high reliability requirements imposed on them. Therefore, we need methods which allow us not only to ensure system correctness but also to integrate design of fault tolerance mechanisms in the development process. In this paper we present a formal approach for the development of fault tolerant location-based mobile agent systems. Our approach is based on stepwise refinement in the Event B framework. We start from an abstract system specification modelling agents together with their communication environment and gradually introduce implementation details in a number of correctness-preserving transformations. Such stepwise development allows us to specify complex system properties, such as fault tolerance, in a structured and rigorous way. Moreover, it enables a formal representation of essential abstractions used in the development of fault tolerant agent systems, including scopes, roles, locations, and agents. Application of the proposed approach results in designing fault tolerant agent systems in which inter-consistency and inter-operability of agents is ensured by construction.