Database of Case Studies Achieved Using CADP

INRES Protocol.

Organisation: Nokia Research Center (Finland)

Method: SDL and LOTOS

Tools used: SDT (Telelogic)
ARA (Tampere University of Technology)
CADP (Construction and Analysis of Distributed Processes)

Domain: Communication Protocols.

Period: 1998.

Size: 3217 states, 13614 transitions (maximal LTS size during compositional generation)

Description: The INRES (Initiator-Responder) protocol is an abridged version of the Abracadabra system described in [ISO-90]. INRES contains many OSI concepts and is therefore very suitable for illustrative purposes. The INRES protocol implements a reliable, connection-oriented data transfer service between two users. The protocol operates above a medium that offers an unreliable data transfer service. The INRES service is not symmetrical: it offers only one way data transmission from an initiating process to a responding process.

Starting from an INRES specification in SDL, the labelled transition system (LTS) of the INRES service (external benaviour of the protocol) has been constructed using two approaches : (a) direct generation, using the SDT Validator tool; (b) compositional generation, using the SDT Validator (for the Initiator and Responder processes), the ARA tools (for the channels and process input queues), and ALDEBARAN (for parallel composition, abstraction, and minimization).

With the approach (a), it was impossible to generate exhaustively the LTS of the protocol using the SDT Validator. Using a bit state hash technique with a low hash collision percentage, SDT Validator generated 388408 states and 1880000 transitions. With the approach (b), the largest LTS constructed during compositional generation had only 3217 states and 13614 transitions.

Conclusions: Compositional generation of LTSs is a useful way to cope with the state-explosion problem. For the INRES case-study, the compositional verification techniques available in the CADP toolset allowed to verify a system which was not possible to verify exhaustively using the SDT Validator tool. Since CADP is able to handle LTSs with over a million states, the compositional style could be used for much larger systems than the INRES protocol.

Publications: [ISO-90] ISO TC97/SC21. "Guidelines for the application of Estelle, LOTOS and SDL". ISO TR 10167, 1990.

[Luukkainen-Ahtiainen-98] M. Luukkainen and A. Ahtiainen. "Compositional Verification of SDL Descriptions". Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC SAM'98 (Berlin, Germany), June 1998.
Available on-line from our FTP site in PDF or PostScript
Contact:
Matti Luukkainen
Department of Computer Science
P.O. Box 26
00014 University of Helsinki
Finland
E-mail: mluukkai@cs.helsinki.fi



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


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


Back to the CADP case studies page