Database of Case Studies Achieved Using CADP

Xpress Transfer Protocol (XTP).

Organisation: Institut Polytechnique de Sévenans, Belfort (FRANCE)

Method: Communicating Finite State Machines (CFSM)

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
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
Tel: +33 (0)3 84 58 31 26
Fax: +33 (0)3 84 58 30 30

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:22:05 2021.

Back to the CADP case studies page