Abstract
The validation is a very important phase in the development cycle of communication protocols. This activity is frequently accomplished by a reachability analysis. In this paper, we are interested in the study of the XTP protocol. The objective is to detect different types of logic errors, before implementation phase, such as deadlock and unspecified reception. To specify and verify XTP protocol, we use two formal models, the communicating finite state machine (S.F.S.M) to describe the behaviour of external transitions and the formal description language LOTOS to study the global behaviour of internal executions between XTP endpoints. In the first model, we validate this protocol by using ValiPro tools to prove the correctness of XTP global behaviour. In the second model, we use LOTOS for studing the protocol data transmission level. Two implementation strategies for data transmission mechanisms are presented which will act on the user data transfer. The choice of moment for sending control packet and its transmission frequency will play a very role in state space level of the reachability tree. To supervise data transmission mechanism and transfer control packets, we propose an implementation method for XTP Timers.