Database of Case Studies Achieved Using CADP

INRES Protocol

Organisation: INT (FRANCE)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Communication Protocols.

Period: 1992

Size: 500 lines of LOTOS.

Description: The INRES (Initiator-Responder protocol), is an abridged version of the Abracadabra protocol used for academic studies and illustrative purposes. It is a connection-oriented, asymmetrical communication protocol featuring many OSI concepts.

The INRES service and protocol have both been specified in LOTOS, compiled into labelled transition systems (LTS) using CAESAR, and then minimized using ALDEBARAN. A large amount of time was devoted to debugging the initial specifications, dealing with the restrictions imposed by CAESAR and introducing simplifications ti limit state space explosion. The obtained LTS have been compared using ALDEBARAN and used as input for a test-sequence generator developed in-house, based on the rural chinese postman tour.

Conclusions: The LOTOS specifier must be concious of the constraints imposed by model generation tools such as CAESAR. The advent of OPEN/CAESAR tools for simulation and deadlock detection has been a great help for analyzing specifications in the absence of a fully generated LTS. After numerous corrections and simplifications, a complete LTS for the protocol was finally obtained. Due to the complexity of that LTS, a formal verification of equivalence between the service and the protocol was considered unrealistic. The test sequence generator has been applied successfully to both the service and the protocol.

Publications: Ana R. CAVALLI, Sung Un KIM and Patrick MAIGRON, "A protocol test sequence generation technique and its application to the Inres protocol", INT Rapport interne de recherche No 92-05-05, May 1992.

Annie Lambert, "Verification de protocoles de Telecommunication Inres et XTP", memoire d'ingenieur IIE CNAM, June 1992.

Mohammed HAMDAOUI, "Utilisation de Caesar dans la verification du protocole de telecommunication INRES", memoire d'ingenieur INT, July 1992.

Kwai Yin SEEK, "The Verification of INRES protocol using CAESAR Toolkit", memoire d'ingenieur INT, July 1992.

Kok Hiong PANG, "Generation of a finite state machine from a LOTOS specification of INRES Protocol using CAESAR", memoire d'ingenieur INT, July 1992.

Contact:
Ana R. CAVALLI
INT
Departement Systemes et Reseaux
Les Epinettes
9 rue Charles Fourier
91011 Evry Cedex
FRANCE
Tel: +33 1 60764427
Fax: +33 1 60783927
E-mail: Ana.Cavalli@int-evry.fr



Further remarks: The LOTOS descriptions as well as explanations on the verification with CADP are available on-line at:
ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_09

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


Last modified: Mon Jul 21 11:38:54 2014.


Back to the CADP case studies page