CADP (Construction and Analysis of Distributed Processes)
770 lines (60% data part, 40% control part)
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.
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.
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
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
Tel: +33 (0)4 76 61 52 83
Fax: +33 (0)4 76 61 52 52
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|