|
| 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: |
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: http://cadp.inria.fr/ftp/demos/demo_09 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