|
| 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 |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
INRIA Rhone-Alpes (FRANCE)
|
|---|---|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
OSI protocols.
|
| Period: |
1995
|
| Size: |
1,400 lines of LOTOS for CCS service 3,000 lines of LOTOS for CCS protocol 15,400 lines of LOTOS for OSI-TP |
| Description: |
CCR (Commitment, Concurrency, and Recovery) belongs to the 7th layer (application layer) of the OSI architecture. The CCR service and protocol have been standardized (ISO standards 9804 and 9805). As a part of the standardization work, there was a work item for producing two formal descriptions in LOTOS of the CCR services and protocols.
In 1995, we have used the CADP tools to these two formal descriptions. Several errors were detected in both descriptions, mostly in the data type part (these errors were discovered by the CAESAR.ADT compiler). These errors have been reported to NPL (National Physical Laboratory, UK), which assumed the editorship role for these formal descriptions. TP (Transaction Processing, also called OSI-TP or DTP, for Distributed Transaction Processing) is a data-base protocol standardized by ISO (standard 8326). A large LOTOS description (15,400 lines) was developed within ISO, in order to provide a formal specification for the OSI-TP protocol. In 1995, we downloaded a draft of this LOTOS description from the FTP server of NPL. By applying the CAESAR and CAESAR.ADT compilers to this draft, 11 errors were found and reported to ISO through AFNOR, the French standardization Institute. For each defect an appropriate solution was proposed.
|
| Conclusion: |
Although if the impact of these case-studies was limited, we believe that they are exemplar from an historical perspective: because it was the original goal of formal description techniques such as LOTOS to be used to describe OSI protocols accurately and unambiguously. In parallel, the CADP tools have been originally designed to be used for computer-aided validation of OSI descriptions. These two case-studies demonstrate that these goals could be achieved.
|
| Publications: |
[Garavel-Sighireanu-95-c]
Defect Report Concerning the LOTOS description of OSI TP protocol
AFNOR, November 1995. Available on-line from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Hubert Garavel INRIA Rhone-Alpes 655 avenue de l'Europe F-38330 Montbonnot Saint-Martin FRANCE Tel: +33 4 76 61 52 24 Fax: +33 4 76 61 52 52 E-mail: Hubert.Garavel@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