Database of Case Studies Achieved Using CADP

Dynamic Reconfiguration Protocol for Agent-Based Applications.

Organisation: INRIA Rhône-Alpes

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Mobile Agents.

Period: 2000-2001

Size: 770 lines (60% data part, 40% control part)

Description: Distributed applications are often complex and must satisfy strong reliability and availability constraints. To avoid stopping an entire distributed application for maintenance operations (repair, upgrade, etc.), it is essential to provide mechanisms allowing distributed applications to be reconfigured at run-time. Such mechanisms should ensure a proper functioning of the application regardless of run-time changes (creation or deletion of agents, replacement of agents, migration of agents across execution sites, modification of communication routes, etc.).

This work considers the dynamic reconfiguration protocol integrated in the AAA (Agents Anytime Anywhere) message-oriented middleware, which allows a flexible, scalable, and reliable development of distributed agent-based applications. This reconfiguration protocol has been experimented in several industrial applications developed in cooperation with BULL (in particular, on an application for managing a set of network firewalls). In the AAA model, the basic software elements are agents, which execute concurrently on several sites and can send and receive messages via communication channels (unidirectional point-to-point links). Agents behave according to an event-reaction scheme: when receiving a message on a channel, an agent executes the appropriate reaction (a piece of code that may update the agent state and/or send messages to other agents).

The dynamic reconfiguration protocol associates to each application a particular agent, called configurator, which is responsible for handling all reconfiguration commands coming from the user. The configurator maintains a view of the application configuration (placement of agents on sites and communication routes between agents), determines if a reconfiguration command can be performed, executes the corresponding actions, and updates the configuration view accordingly. The protocol implements the following reconfiguration commands: ADD (addition of a new agent to the application), DELETE (removal of an agent from the application), MOVE (migration of an agent to another site), BIND and REBIND (creation and modification of a communication channel between two agents).

Starting from a prototype implementation in JAVA, a LOTOS specification of the dynamic reconfiguration protocol was obtained and validated using the CADP toolbox. Several instances of the protocol were analysed, involving a finite number of sites, agents, and communication channels. The corresponding Labeled Transition Systems were generated with the CAESAR compiler and reduced using the BCG_MIN tool. Additionally, a set of 10 correctness properties expressing the safety and liveness of each reconfiguration primitive were identified and formulated in regular alternation-free mu-calculus. All properties were verified on each instance of the protocol using the EVALUATOR 3.0 model-checker of CADP.

Conclusions: The dynamic reconfiguration protocol included in the AAA middleware for construction of distributed agent-based applications was formally specified in LOTOS. The specification obtained provides a non-ambiguous description of the protocol and a basis for future development and experimentation of new reconfiguration primitives. This experiment increased the confidence in the correctness of the protocol and assessed the usefulness of LOTOS for modeling distributed applications based on mobile agents.

Publications: [Aguilar-Garavel-Mateescu-dePalma-01] Manuel Aguilar Cornejo, Hubert Garavel, Radu Mateescu, and Noel de Palma. "Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications". Proceedings of the 3rd IFIP WG 6.1 International Working Conference on Distributed Applications and Interoperable Systems DAIS'2001 (Krakow, Poland), pp. 229-242, September 2001. Full version available as INRIA Research Report RR-4222, INRIA, July 2001.
Available on-line from http://cadp.inria.fr/publications/Aguilar-Garavel-et-al-01.html
Contact:
Radu Mateescu
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
FRANCE
Tel: +33 (0)4 76 61 52 83
Fax: +33 (0)4 76 61 52 52
E-mail: Radu.Mateescu@inria.fr
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 18:02:10 2018.

Back to the CADP case studies page