CADP (Construction and Analysis of Distributed Processes)
Up to 7,200 lines of LOTOS, 1,600 lines of SVL,
and 70 concurrent processes.
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.
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:
[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,
Available on-line from http://cadp.inria.fr/publications/Tronel-Lang-Garavel-03.html
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
Tel: +33 (0)4 76 61 52 24
Fax: +33 (0)4 76 61 52 52
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies