Database of Case Studies Achieved Using CADP

CCR (Commitment, Concurrency, and Recovery) and OSI-TP (Transaction Processing)

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 our FTP site in PDF or PostScript
Hubert Garavel
INRIA Rhone-Alpes
655 avenue de l'Europe
F-38330 Montbonnot Saint-Martin
Tel: +33 4 76 61 52 24
Fax: +33 4 76 61 52 52

Further remarks:

This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page