CADP (Construction and Analysis of Distributed Processes)
500 lines of LOTOS.
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
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.
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.
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,
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.
Ana R. CAVALLI
Departement Systemes et Reseaux
9 rue Charles Fourier
91011 Evry Cedex
Tel: +33 1 60764427
Fax: +33 1 60783927
The LOTOS descriptions as well as explanations on the verification with
CADP are available on-line at: |
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies