Database of Case Studies Achieved Using CADP

Compositional Verification of the ScalAgent Deployment Protocol.

Organisation: INRIA Rhône-Alpes

Method: LOTOS

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

Domain: Mobile Agents.

Period: 2001-2003

Size: Up to 7,200 lines of LOTOS, 1,600 lines of SVL, and 70 concurrent processes.

Description: This work was funded in the scope of RNTL project PARFUMS (Pervasive Agents for Reliable and Flexible UPS Management Services), an industrial project involving three companies (MGE-UPS, SILICOMP Research Institute, and SCALAGENT Distributed Technologies), and the VASY research group at INRIA.

The goal of PARFUMS was to develop embedded software for UPS (Uninterruptible Power Supply) in order to improve management (installation, repair, and monitoring of remote equipments) on large scale sites. To master the complexity induced by the distribution of applications, the project relies on the SCALAGENT platform for embedded systems, written in JAVA, to configure, deploy, and reconfigure software. This case study is about the modeling of the SCALAGENT deployment protocol and its verification using the CADP toolbox.

To ensure scalability, the SCALAGENT deployment protocol relies on a tree-like hierarchy of distributed agents communicating asynchronously by means of events. The protocol uses two kinds of agents, namely containers, located at the leaves of the tree hierarchy, which encapsulate components written in any language and act as interfaces with the rest of the protocol, and controllers, located at higher nodes of the tree hierarchy, which handle communications with their parent and children agents. Controllers are specified by a workflow of activities, themselves structured as a tree. To describe distributed configurations, the SCALAGENT infrastructure relies on the use of an XML DTD named XOLAN. An XOLAN configuration describes a set of agents, their geographical distribution, as well as their dependencies in terms of provided and required services, which rule the way the deployment must be performed.

To enable verification of several configurations without writing one complex LOTOS specification for each configuration, an automatic translator has been developed. This translator takes an XOLAN configuration and produces both the LOTOS specification corresponding to this configuration (each activity being translated into a separate process in the generated code), and an SVL script to perform the verification automatically.

To cope with the complexity of the protocol, compositional verification methods have been used. They consist in dividing the system to be verified in several components, which will be analyzed separately. Then the results of the separate analyses are combined together to analyze the whole system.

The decomposition chosen in this case study exploits two essential properties of the SCALAGENT deployment protocol: communications are pairwise between an activity and each of its subactivities, and messages do not accumulate indefinitely in a communication medium (i.e., FIFO buffers and bags). Therefore, communication media can be described as finite processes containing a bounded number of messages belonging to a finite set of possible values, and the communications can be handled using one medium for each pair of communicating activities. This approach fits well with compositional verification, because the synchronizations between communicating processes can be taken into account earlier in the verification process. Hiding messages as soon as they have been synchronized permits to obtain better reductions by minimization tools.

Conclusions: The use of compositional verification allowed to check significantly complex finite configurations (from 31 to 71 concurrent processes) within a reasonable amount of time (less than 20 minutes). Two main conclusions can be drawn from the experiments:
  • Although the high number of concurrent processes could potentially lead to huge state space (up to 9.10^68 states if its size is estimated by multiplying the numbers of states of the minimized LTSs corresponding to all activities and media for a given configuration), compositional verification allows to keep the state space to a tractable size (less than 10^6 states).

  • Given the large number of intermediate files (several hundreds), these experiments would not have been possible without the SVL language and associated compiler.
In addition, formal modeling of the protocol allowed to find several ambiguities in the reference specification and the verification work exhibited an undocumented assumption (synchrony of communications) of crucial importance for a proper functioning of the protocol.

Publications: [Tronel-Lang-Garavel-03] Frédéric Tronel, Frédéric Lang, and Hubert Garavel. "Compositional Verification using CADP of the ScalAgent Deployment Protocol for Software Components". Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems FMOODS'2003 (Paris, France), P. Stevens and U. Nestmann, editors, Lecture Notes in Computer Science, Springer-Verlag, 2003. Full version available as INRIA Research Report RR-5012, INRIA, September 2003.
Available on-line from http://cadp.inria.fr/publications/Tronel-Lang-Garavel-03.html
Contact:
Hubert Garavel
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
FRANCE
Tel: +33 (0)4 76 61 52 24
Fax: +33 (0)4 76 61 52 52
E-mail: Hubert.Garavel@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