Protocol analysis and verification methods, application to the Xpress Transport Protocol 4.0

  • O. Catrina
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)


The paper presents methods for protocol analysis and verification, based on the observation of simulations of a formal description, written in Estelle. The methods were experimented during the development of an Estelle specification for the new definition of the Xpress Transport Protocol (XTP), revision 4.0. Starting from a set of proposed modifications of the previous revision, the development included the identification and the verification of the solutions for accomplishing the protocol functions, using the new definitions of the protocol mechanisms.


Communication software engineering high speed transport protocols formal description technique Estelle validation simulation. 


  1. Algayres, B., Colho, V., Doldi, L., Garavel, H., Lejeune, Y., Rodriguez, C (1991) Vésar: Un outil pour la spécification et la vérification formelle de protocoles. CFIP’91, Ingénierie des Protocoles, Hermes, Paris.Google Scholar
  2. Budkowski, S. (1992) Estelle Development Toolset. Computer Networks and ISDN Systems Journal, Special Issue on FDT Concepts and Tools, vol. 25, no. 1.Google Scholar
  3. Catrina, O. (1995) Utilization of the synchronization mechanism in XTP 4.0, XTP Forum Research Affiliate Annual Report 1994, XTP Forum, Santa Barbara, Ca, USA.Google Scholar
  4. Dembinski, P., Budkowski, S. (1987) Simulating Estelle specifications with time parameters. 7th Workshop on Protocol Specification, Testing and Verification, Zurich.Google Scholar
  5. Groz, R (1989) Vérification de propriétés logiques des protocoles et systemes répartis par obsrvation de simulations. These de doctorat, Université de Rennes I.Google Scholar
  6. Holtzman, G. (1991) Design and Validation of Computer Protocols Prentice Hall.Google Scholar
  7. ISO (1989) Estelle - A Formal Description Technique based on Extended State Transition Model, IS 9074.Google Scholar
  8. Jard, C., Jeron, Th. (1991) Bounded memory algorithms for verification on-the-fly. CAV 91: Symposium on Computer Aided Verification, Aalborg, Denmark.Google Scholar
  9. Lallet, E., Dembinski, P., Mouchel La Fosse, J.P., Alkhechi, B., Gardie, M., Catrina, O., Budkowski, S. (1994) Validation of the Xpress Transfer Protocol. The 0S195 Transport Service with Multimedia Support, Springer Verlag, Berlin, pg. 42–63.CrossRefGoogle Scholar
  10. Pageot, J.M. (1989) Guider la simulation pour valider les protocoles. These de doctorat, Université de Rennes I.Google Scholar
  11. Vissers, C., van Sinderen, M., Pires, L. (1993) What Makes Industries Believe in Formal Methods. Protocol Specification, Testing and Verification XIII, Elsevier.Google Scholar
  12. Weaver, A. (1994) The Xpress Transfer Protocol, Computer Communications, vol. 17, no. 1.Google Scholar
  13. West, C.H. (1986) Protocol validation by random state exploration. 6th Workshop on Protocol Specification, Testing and Verification, Montreal.Google Scholar
  14. XTP (1992) Xpress Transfer Protocol definition revision 3. 6, Protocol Engines Incorporated, Santa Barbara, CA, USA.Google Scholar
  15. XTP (1995) Xpress Transport Protocol specification revision 4.0, XTP Forum, Santa Barbara, CA, USA, March 1, 1995.Google Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • O. Catrina
    • 1
  1. 1.Electronics and Telecommunications DepartmentPolitehnica University of BucharestBucharestRomania

Personalised recommendations