Bull-IMAG (Grenoble, France) and INRIA Rhone Alpes
CADP (Construction and Analysis of Distributed Processes)
Distributed Systems, Cooperative applications.
3,000 lines of LOTOS.
All the ideas on the architecture and protocols of a synchronous
groupware development ("What You See Is What I See") are generally
expressed informally, and there is no way to actually test the
consistency of architectural choices, or protocols combination without
The aim of this work is to extend an existing development with a formal description of its architecture and functionalities. We first specified in LOTOS the architecture itself and verified some generic properties on this architecture. Then it is possible to actually analyze and test the integration of different protocols for the management of collaboration. The formal specification is derived from a component based description: the actual implementation of the framework.
We define some important properties for cooperative applications, and then show how they can be verified using the CADP toolbox.
The verification phase of the framework description is not a trivial
process as the model generated is large (over 20 million states at the
beginning of the verification process). We have used with significant
success the "on the fly" and BDD based extensions of the CADP toolbox,
combined with compositional model generation.
Our aim was to introduce in a component's description behavioural specifications as an abstraction of its dynamic behaviour. The introduction of these behavioural specifications will help to enforce an important need, which is the ability to reuse software components, or to replace a software component by another without interferences.
Available on-line from
and on our FTP site in PDF or PostScript
2, avenue de Vignate
Tel: +(33) 4 76 63 48 59
Fax: +(33) 4 76 63 48 50
Y. Laribi (Bull-Imag) has used CADP to validate three Failure Management
Protocols in a group allowing dynamic connections-deconnections.
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies