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 http://cadp.inria.fr/publications/Kerbrat-BenAtallah-95.html and on the CADP Web site in PDF or PostScript
Contact:	Alain Kerbrat VERIMAG Centre Equation 2, avenue de Vignate F-38610 Gieres FRANCE Tel: +(33) 4 76 63 48 59 Fax: +(33) 4 76 63 48 50 E-mail: Alain.Kerbrat@imag.fr
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: http://cadp.inria.fr/case-studies

Back to the CADP case studies page