APERO (data type facilities)
CADP (Construction and Analysis of Distributed Processes)
EUCALYPTUS (graphical user interface)
Distributed Knowledge Bases.
- 1400 lines of LOTOS (using APERO concise data type definitions)
- 4 man-months.
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.
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.
"Specification and Validation of the CO4 distributed knowledge system
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
655 avenue de l'europe
38330 Montbonnot Saint Martin
tel : +33-4188.8.131.52
fax : +33-4184.108.40.206
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|