Institut Polytechnique de Sévenans, Belfort (FRANCE)
Communicating Finite State Machines (CFSM)
ValiPro (Validation Protocols)
CADP (Construction and Analysis of Distributed Processes)
3347 states (first strategy) and 2963 states (second strategy)
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
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.
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.
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 our FTP site in PDF or PostScript
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: http://cadp.inria.fr/case-studies|