|
| 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: |
Institut Polytechnique de Sévenans, Belfort (FRANCE)
|
|---|---|
| Method: |
Communicating Finite State Machines (CFSM)
LOTOS |
| Tools used: |
ValiPro (Validation Protocols) CADP (Construction and Analysis of Distributed Processes) |
| Domain: |
Communication Protocols.
|
| Period: |
1998.
|
| Size: |
3347 states (first strategy) and 2963 states (second strategy)
|
| Description: |
XTP (Xpress Transfer Protocol) is a high-speed transport protocol
standardized by ISO. The mechanisms of XTP are specifically designed
for high bandwidth, low delay and low errors rate communication.
The goal of this case-study is to analyse the XTL protocol using formal
methods, in order to detect possible design errors before the
implementation phase.
The global XTP behaviour has been described using Communicating Finite State Machines (CFSMs) and analyzed using ValiPro. The XTP endpoints, modeled as two automata, are connected by communication channels considered as unidirectional, reliable and FIFO. Validation has been performed using two reachability methods, for a bounded size of the FIFO channels. The global behaviour of XTP has been found correct. The data transmission level of the protocol has been specified in LOTOS and validated using CADP, for a bounded number of data messages present in the protocol. Two strategies for user data transmission, differing in the choice and frequency of control packets, have been considered. The analysis with CADP did not reveal logical errors in the design: all messages are succesfully transmitted from the sender to the receiver. However, the second strategy led to a smaller state space, thus being more efficient w.r.t. the number of messages. |
| Conclusions: |
Formal description languages are suitable for describing and analysing
protocols, especially due to their ability for modelling data variables
and parameters. The use of LOTOS and CADP enabled to compare two
versions of XTP based on different strategies of data transmission.
|
| Publications: |
[PEI-92]
Protocol Engines Inc.
"XTP Protocol Definition."
Revision 3.6, January 1992.
[Benslimane-Abouaissa-98] A. Benslimane and A. Abouaissa. "XTP Specification and Validation with LOTOS". Proceedings of the Western MultiConference WMC'98, Communication Networks and Distributed Systems Modeling and Simulation CNDS'98 (San Diego, California, USA), pages 121-127, January 1998. Available online from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Abderrahim Benslimane Laboratoire de Recherche en Informatique de Sévenans Université de Technologie de Belfort Montbéliard Site de Sévenans F-90010 Belfort Cedex France Tel: +33 (0)3 84 58 31 26 Fax: +33 (0)3 84 58 30 30 E-mail: Abder.Benslimane@utbm.fr |
| 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