Database of Case Studies Achieved Using CADP

The Co4 Distributed Knowledge System

Organisation: INRIA Rhone-Alpes

Method: LOTOS

Tools used: APERO (data type facilities)
CADP (Construction and Analysis of Distributed Processes)
EUCALYPTUS (graphical user interface)


Domain: Distributed Knowledge Bases.

Period: Feb-May 1997.

Size: - 1400 lines of LOTOS (using APERO concise data type definitions)
- 4 man-months.

Description: Co4 is a computer environment dedicated to the building of a distributed knowledge base. In particular, communication between Co4 entities follow a consensual decision protocol inspired from paper reviewing policies. This protocol has been specified in LOTOS. To obtain finite state spaces of tractable size, we have considered a fixed number of entities (2 to 5 bases) and particular execution scenarios only. The CADP tools have been used to verify different safety and liveness properties. The verification work has confirmed an announced violation of knowledge consistency and has put forth a case of inconsistent hierarchy, four cases of unexpected message reception and some further local corrections in the definition of the protocol.

Conclusions: The specification of Co4 ranges among medium-size LOTOS specifications. This case study shows how significant results can be obtained for real-size systems, thanks the computing power of modern computers, the level of sophistication of verification tools and a fair practical expertise in these tools.

Publications: [Pecheur-97] Charles Pecheur. "Specification and Validation of the CO4 distributed knowledge system using LOTOS". In Proceedings of the 12th IEEE Conference on Automated Software Engineering (Incline Village, Nevada), November 1997. Extended version available as INRIA Research Report RR-3259, September 1997.
Available on-line from http://cadp.inria.fr/publications/Pecheur-97.html
Contact:
Charles Pecheur
INRIA Rhone-Alpes
655 avenue de l'europe
38330 Montbonnot Saint Martin
France
tel : +33-476.61.52.98
fax : +33-476.61.52.52
E-mail : Charles.Pecheur@inria.fr



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Thu Oct 8 14:28:34 2015.


Back to the CADP case studies page