|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 |
Back to the CADP case studies page