Database of Case Studies Achieved Using CADP

Framework for Groupware Development

Organisation: Bull-IMAG (Grenoble, France) and INRIA Rhone Alpes

Method: LOTOS

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

Domain: Distributed Systems, Cooperative applications.

Period: 1995

Size: 3,000 lines of LOTOS.

Description: 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 implementing them.

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.

Conclusions: 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.

Publications: [KerbratBenAtallah95] Available on-line from
and on the CADP Web site in PDF or PostScript

Alain Kerbrat
Centre Equation
2, avenue de Vignate
F-38610 Gieres
Tel: +(33) 4 76 63 48 59
Fax: +(33) 4 76 63 48 50

Further remarks: 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:

Last modified: Thu Feb 11 12:22:05 2021.

Back to the CADP case studies page