Abstract
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.
Top2 Background: Cama Middleware
Context-Aware Mobile Agents (CAMA) systems (Iliasov & Romanovsky, 2005; Arief, Iliasov & Romanovsky, 2006; Iliasov, Romanovsky et al., 2007) are defined via a set of abstractions and operations modeling inter-agent communication and operability. The primary goal of defining a CAMA system is to offer programmers a formally-verified basis for rapid development of mobile agent software in a disciplined and structured way.
CAMA inter-agent communication is based on the LINDA paradigm (Gelernter, 1985). LINDA provides a set of coordination primitives that can be used for coordination of several independently running pieces of software. Since LINDA is language independent, it became quite popular andits coordination primitives have been implemented in many programming languages. Moreover, LINDA supports asynchronous and anonymous agent communication and hence is well-suited for mobile agent systems.
A CAMA system consists of a set of locations. The main role of a location is to provide the inter-agent communication service to its client agents. The communication service is based on a shared blackboard supporting LINDA operations.
Key Terms in this Chapter
Multi-Agent Systems: Are systems composed of multiple autonomous agents, such as software programs or robots, that interact with each other. Their interactions can be either cooperative, that is, they can share a common goal, or selfish, that is, they can pursue their own interests. Multi-agent systems can be used to solve complex problems in areas such as disaster response, online trading and social structure modeling.
Context-Awareness: Is a term used for entities such as devices or programs that have information about the circumstances under which they operate and can react to changes in these circumstances.
Decomposition: Is the breaking down of a program design or code into a set of component parts (e.g., modules). The decomposition is guided by a set of design principles or criteria that the identified parts should reflect.
Program Refinement: Is a verifiable transformation of an abstract (i.e., high-level) formal specification into a concrete (i.e., low-level) specification or an executable program. Stepwise refinement allows the refinement of a program to be done in stages.
Mobile Agents: Is a term used to describe software agents that can migrate (move) from one computing location (e.g., process or computer) to another and continue its execution on its destination.
B Method: Is an approach for rigorous or formal development of software using the notion of Abstract Machines to specify and design software systems.
Formal Specification: Is a specification written in a formal language with a precise syntax and a well-defined semantics based on well-established mathematical concepts. This mathematical description of software or hardware describes what the system should do without necessarily providing details on how the system should do it.