What is Program Refinement

Mobile agent systems are complex distributed systems that are dynamically composed of autonomous agents. Since agents are often developed independently, they may lack interoperability, i.e., do not communicate in a correct way. In this chapter, the authors propose a formal approach to ensuring interoperability of agents implemented by independent developers. The essence of the approach is the decomposition of a specification of a multi-agent application into a set of specifications of agent roles. While decomposing the specification, they explicitly define the communication mechanisms between the agents. To ensure interoperability, the implementation of each agent should adhere to its formal specification. However, each agent can be implemented completely independently, i.e., without knowing the specifications of other agents. The authors use refinement in the Event-B framework to define formally the process of decomposing a multi-agent application into a set of interacting roles. The approach is illustrated by a case study involving the development of an electronic auction.