|
| 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 Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 the CADP Web 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 |
Back to the CADP case studies page