Skip to main content
SpringerLink
Log in
Book cover

Current Trends in Concurrency pp 208–265Cite as

Design, specification and validation of hierarchies of protocols in distributed systems

  • Chapter
  • First Online:

  • 141 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 224))

Abstract

This paper addresses the design, specification and validation of the hierarchy of software which is needed when developing complex distributed systems. The main specificities of the design are emphasized and related to a reference model, the OSI ISO/CCITT reference model. A methodological approach for specification and validation is given. In order to show the possible resulting complexity, an exemple, the transport layer, is discussed.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

VII — Bibliography

  1. JP. ANSART, V. CHARI, D. SIMON, "From formal description to automated implementation using PDIL", Protocol Specification, Testing and Verification, III, North Holland, 1983, H. Rudin — C. West Editors.

    Google Scholar 

  2. JP. ANSART, "Refinement — From specification to implementation — Issues and tools for protocol specification", Advanced Course on Distributed Systems, Inst. Informatik, Univ. of Muchen, April 1984.

    Google Scholar 

  3. JM. AYACHE, JP. COURTIAT, "LC/1, A specification and implementation language for protocols", Protocol Specification, Testing and Verification, III, North Holland, 1983, H. Rudin — C. West Editors.

    Google Scholar 

  4. JM. AYACHE, JP. COURTIAT, M. DIAZ, "REBUS: a fault-tolerant distributed system for industrial real time control", IEEE T.C., Special Issue on Fault-Tolerant Computing, Juillet 1982.

    Google Scholar 

  5. P. AZEMA, B. BERTHOMIEU, P. DECITRE, "The design and validation by Petri nets of a mechanism for the invocation of remote servers", Proc. of IFIP Congress, Melbourne, Octobre 1980.

    Google Scholar 

  6. B. BERTHOMIEU, M. MENASCHE, "Analysis by state enumeration of time Petri nets", Proc. of the IFIP Congress, Paris, Septembre 1983.

    Google Scholar 

  7. B. BERTHOMIEU, "Algebraic specification of communication protocols", Research Report ISI-RR-81-98, also Technical Report LAAS-CNRS, 81.T.26, Octobre 1981.

    Google Scholar 

  8. G. BERTHELOT, R. TERRAT, "Petri nets theory for the correctness of protocols", 2nd. Europ. Workshop on Appl. & Theory of Petri nets, Bad Honnef (F.R.G.), September 1981, pp.31–58, also 2nd Int. Workshop on Protocol Specification Testing and Verification, Idyllwild Los Angeles, May 1982, North-Holland, 1982, C. Sunshine Ed., also IEEE Trans. on Comm. vol. COM-30, no.12, December 1982.

    Google Scholar 

  9. J. BILLINGTON, "Specification of the transport service using numerical Petri nets", 2nd Int. Workshop on Protocol Specification, Testing and Verification, Idyllwild Los Angeles, Mai 1982, North-Holland, 1982, C. Sunshine Editor.

    Google Scholar 

  10. G.V. BOCHMANN, "Finite state description of communication protocols", Conf. Computer Network Protocols, Liège, 1978, also in Computer Networks 2, 1978, pp. 361–372.

    Google Scholar 

  11. G.V. BOCHMANN, "A general transition model for protocols and communication services", IEEE Trans. on Communications, vol. COM-28, no. 4, April 1980, pp.643–650.

    Google Scholar 

  12. G.V. BOCHMANN, C.A. SUNSHINE, "Formal methods in communication protocol design", IEEE Trans. on Communications, vol. COM-28, no. 4, April 1980, pp. 624–631.

    Google Scholar 

  13. E. BRINKSMA, "The specification language LOTOS", 5th Int. Workshop on Protocol Specification, Testing and Verification, Toulouse, June 1985, NORTH HOLLAND, M. Diaz Editor, 1986.

    Google Scholar 

  14. J.P. COURTIAT, J.M. AYACHE, B. ALGAYRES, "Petri Nets are Good for Protocols", SIGCOMM 84 Symposium; also in Computer Communications Review, 14, No.2, 1984.

    Google Scholar 

  15. A.S. DANTHINE, "Protocol representation with finite-state models", IEEE Trans. on Communications, vol. COM-28, no. 4, pp. 632–643.

    Google Scholar 

  16. M. DIAZ, "Modeling and analasys of communication and cooperation protocols using Petri net based models", Tutorial paper, Proc. of the IFIP WG 6.1 Second Int. Workshop on Protocol Specification, Testing and Verification, Idyllwild-CA, Mai 1982, C. Sunshine Editor, North-Holland 1982; also Computer Networks, vol. 6, no. 6, December 1982.

    Google Scholar 

  17. M. DIAZ, J.P. COURTIAT, B. BERTHOMIEU, J.M. AYACHE, "Status of Petri net based models for protocols", IEEE Int. Conf. on Communications, ICC 83, Boston, June 1983.

    Google Scholar 

  18. M. DIAZ, G. GUIDACCI DA SILVEIRA, "On the specification and validation of protocols by temporal logic and nets", Proceeding of the IFIP 83 Congres, Paris, September 1983.

    Google Scholar 

  19. M. DIAZ, CH. VISSERS, JP. ANSART, "SEDOS, Software Environment for the Design of Open distributed Systems", ESPRIT Week, Brussels, September 1985.

    Google Scholar 

  20. H.J. GENRICH, K. LAUTENBACH, "The analysis of distributed systems by means of predicate/transition nets", Semantics of Concurrent Computation, Evian 1979, G. Kahn Editor, Lect. Notes in Computer Sciences, vol. 70, Springer Verlag 1979, pp. 123–146.

    Google Scholar 

  21. S.L. GERHART et al, "An overview of AFFIRM: a specification and verification system", Proc. of the IFIP Congress, October 1980, pp. 343–348.

    Google Scholar 

  22. D.I. GOOD, R.M. COHEN, "Verifiable communications processing in GYPSY", Proc. of COMPCON 78, IEEE, September 1978.

    Google Scholar 

  23. B.T. HAILPERN, S.S. OWICKI, "Modular verification of computer communication protocols", IEEE T. on Communications, vol. COM-31, no. 1, January 1983, pp. 56–68.

    Google Scholar 

  24. IEEE — Local Area Networks, ANSI/IEEE Family of Standards 802 IEEE Std 802.1–802.5

    Google Scholar 

  25. ISO/TC/97/SC 16/537, "Data Processing — Open Systems Interconnection — Basic Reference Model", December 1980.

    Google Scholar 

  26. ISO/TC 97/SC 16, "OSI — Transport Service Definition", January 1984.

    Google Scholar 

  27. ISO/TC 97/SC 16, "OSI — Connection Oriented Transport Protocol Specification", January 1986.

    Google Scholar 

  28. ISO/TC 97/SC 21/ WG1-FDT/SG-B, "Estelle, A Formal Description Technique Based on an Extended State Transition Model", December 1986.

    Google Scholar 

  29. ISO/TC 97/SC 21/ WG1-FDT/SG-C, "LOTOS, a Temporal ordering specification", December 1986.

    Google Scholar 

  30. G. JUANOLE, B. ALGAYRES, J. DUFAU, "On Communications Protocol Modelling and Design" LN in CS, Springer Verlag, 188, Advances in Petri nets 1984, G. Rozenberg Editor.

    Google Scholar 

  31. G. JUANOLE, "Numbering Schemes Required for Reliable Data Transfer in Computers Networks, IEEE INFOCOM 85, March 1985, Washington.

    Google Scholar 

  32. R.M. KELLER, "Formal verification of parallel programs", Com. ACM 19–7, Juillet 1976, pp. 371–384, vol. 19, no. 7.

    Google Scholar 

  33. R.J. LINN, "The features and facilities of ESTELLE", 5th Int. Workshop on Protocol Specification, Testing and Verification, Toulouse, June 1985, NORTH HOLLAND, M. Diaz Editor, 1986.

    Google Scholar 

  34. MAP, MAP Specification, General Motors Technical Center, 1986.

    Google Scholar 

  35. A. PEDROZA, "Contribution à la définition d'un environnement pour la conception de protocoles", Doctorat Thesis, Univ. Paul-Sabatier, Toulouse, July 1985.

    Google Scholar 

  36. R.R. RAZOUK, G. ESTRIN, "Modelling and verification of communication protocols in SARA: the X.21 interface", IEEE Trans. on Computers, vol. C-29, no. 12, Decembre 1980, pp. 1038–1051.

    Google Scholar 

  37. R.L. SCHWARTZ, P.M. MELLIAR-SMITH, "From state machine to temporal logic: specification methods for protocol standards", Tutorial Paper, 2nd Workshop on Protocol Specification, Testing and Verification, Idyllwild Los Angeles, Mai 1982, North-Holland, 1982, C. Sunshine Ed., also IEEE Trans. on Communications, COM-30, no. 12, December 1982, pp. 2486–2496.

    Google Scholar 

  38. P. STUDNITZ, "Transport Protocols: Their performance and status in international standardization (July 1982), Computer Networks 7 pp.25–35, 1983.

    Google Scholar 

  39. C.A. SUNSHINE, "Survey of protocol definition and verification techniques", Computer Networks, 2, 1978, pp.346–350.

    Google Scholar 

  40. F.J.W. SYMONS, "Representation, analysis and verification of communication protocols", Research Report 7380, Telecom. Australia, 1980.

    Google Scholar 

  41. D.T. THOMPSON, C.A. SUNSHINE, R.W. ERICKSON, S.L. GERHART, D. SCHWABE, "Specification and verification of communication protocols in AFFIRM using state transition models", Research Report ISI-RR-81-88, USC, Inf. Sc. Institute, Mars 1981.

    Google Scholar 

  42. Ch. VISSERS, L. LOGRIPPO, "The importance of the concept of service", 5th Int. Workshop on Protocol Specification, Testing and Verification, Toulouse, June 1985, NORTH HOLLAND, M. Diaz Editor, 1986.

    Google Scholar 

  43. C. WEST, P. ZAFIROPULO, "Automated validation of a communication protocol: the CCITT X.21 recommendation", IBM J.R. and Develop., vol. 22, Janvier 1978, pp. 60–71.

    Google Scholar 

  44. H. ZIMMERMAN, "OSI reference model. The ISO model of architecture for open systems interconnection", IEEE Trans. on Communications, vol. COM-28, Avril 1980.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Jean-Pierre COURTIAT Aloysio PEDROZA, France

    Michel Diaz

  2. 7, avenue du Colonel-Roche, 31077, Toulouse, France

    Laas du Cnrs

Authors
  1. Michel Diaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laas du Cnrs
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Diaz, M., du Cnrs, L. (1986). Design, specification and validation of hierarchies of protocols in distributed systems. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Current Trends in Concurrency. Lecture Notes in Computer Science, vol 224. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027042

Download citation

  • DOI: https://doi.org/10.1007/BFb0027042

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16488-3

  • Online ISBN: 978-3-540-39827-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation