Skip to main content

Time in Formal Protocol Specifications

  • Conference paper
Kommunikation in Verteilten Systemen I

Part of the book series: Informatik-Fachberichte ((INFORMATIK,volume 95))

Abstract

The need for formal, machine-readable specification of the protocols used in distributed computer systems is widely accepted. In these formal protocol specifications relatively little attention has been paid to the problem of including time — the time it takes to execute various portions of the protocol as well as explicit values for timeouts. In this tutorial, models for including time are reviewed. Techniques for analyzing these models are then discussed. A comprehensive bibliography is included.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Aggarwal and R. P. Kurshan, “Modelling elapsed time in protocol specification,” Proc. Workshop on Protocol Specification, Testing, and Verification, III, Rüschlikon, Switzerland, May 1983, (North-Holland, Amsterdam, 1983) pp. 51–62.

    Google Scholar 

  2. W. L. Bauerfeld, “Description, verification, and performance prediction of computer network protocols,” Proc. INWG/NPL Workshop on Protocols, Volume 1, Teddington, England, May 27–29, 1981, pp. 253–269.

    Google Scholar 

  3. W. L. Bauerfeld, “Protocol performance prediction,” Proc. International Conference on Communications, IEEE, Boston, Mass., June 20–23, 1983, pp. 1311–1315.

    Google Scholar 

  4. B. Beizer, “Analytical techniques for the statistical evaluation of program running time,” Proc. Fall Joint Computer Conference, 1970, pp. 519–524.

    Google Scholar 

  5. T. Bolognesi and H. Rudin, “On the analysis of time-constrained protocols by network flow algorithms,” Proc. Workshop on Protocol Specification, Testing, and Verification, IV, Sky Top, Pennsylvania, June 1984, (North-Holland, Amsterdam, 1984).

    Google Scholar 

  6. J. E. Coolahan, Jr. and N. Roussopoulos, “Timing requirements for time-driven systems using augmented Petri nets,” IEEE Trans. Software Eng., Vol. SE-9, No. 5, Sept. 1983, pp. 603–616.

    Article  Google Scholar 

  7. M. Diaz, “Modeling and analysis of communication and cooperation protocols using Petri-net based models,” Computer Networks, Vol. 6, 1982, pp. 419–441.

    MATH  Google Scholar 

  8. M. G. Gouda, “Protocol machines: towards a logical theory of communication protocols,” PhD. thesis, University of Waterloo, Jan., 1978 (see especially Chapter 11).

    Google Scholar 

  9. Y. W. Han, “Performance evaluation of a digital system using a Petri net-like approach,” Proc. National Electronics Conference, Chicago, 1978, pp. 166–172.

    Google Scholar 

  10. P. Kritzinger, “Analyzing the time efficiency of a communication protocol,” Proc. Workshop on Protocol Specification, Testing, and Verification, IV, Sky Top, Pennsylvania, June 1984, (North-Holland, Amsterdam, 1984).

    Google Scholar 

  11. P. Kritzinger, “A performance model of the OSI communication architecture,” IBM Zurich Research Laboratory Research Report, Rüschlikon, Switzerland, Nov., 1984.

    Google Scholar 

  12. M. Menasche and B. Berthomieu, “Time Petri nets for analyzing and verifying time dependent communication protocols,” Proc. of the Workshop on Protocol Specification, Testing, and Verification, III, Rüschlikon, Switzerland, May 1983, (North-Holland, Amsterdam, 1983) pp. 161–172.

    Google Scholar 

  13. P. Merlin and D. J. Farber, “Recoverability of communication protocols: implications of a theoretical study,” IEEE Trans. Commun., Vol. COM-24, Sept. 1976, pp. 1036–1043.

    Article  MathSciNet  Google Scholar 

  14. R. Milner, “A Calculus of Communicating Systems,” Lecture Notes in Computer Science, (Springer Verlag, Berlin, 1980).

    MATH  Google Scholar 

  15. M. K. Molloy, “Performance analysis using stochastic Petri nets,” IEEE Trans. Computers, Vol. C-31, Sept. 1982, pp. 913–917.

    Article  Google Scholar 

  16. N. Nounou and Y. Yemini, “Algebraic specification-based performance analysis of communication protocols,” Proc. Workshop on Protocol Specification, Testing, and Verification, TV, Sky Top, Pennsylvania, June 1984, (North-Holland, Amsterdam, 1984).

    Google Scholar 

  17. J. L. Peterson, “Petri Nets,” Computing Surveys, Vol. 9, September 1977, pp. 223–252.

    Article  MathSciNet  MATH  Google Scholar 

  18. C. V. Ramamoorthy and G. S. Ho, “Performance evaluation of asynchronous concurrency systems using Petri nets,” IEEE Trans. Software Eng., Vol. SE-6, Sept. 1980, pp. 440–449.

    Article  MathSciNet  Google Scholar 

  19. C. Ramchandani, “Analysis of asynchronous concurrent systems by timed Petri nets,” Ph.D. Thesis, M. I. T., Dept. of E. E., AD-775618, July, 1973.

    Google Scholar 

  20. R. R. Razouk and C.V. Phelps, “Performance analysis using timed Petri nets,” Proc. of the Workshop on Protocol Specification, Testing, and Verification, IV, Sky Top, Pennsylvania, June 1984, (North-Holland, Amsterdam, 1984).

    Google Scholar 

  21. H. Rudin and C.H. West, “A validation technique for tightly-coupled protocols,” IEEE Trans. Computers, Vol. C-31, July, 1982, pp. 630–636.

    Article  Google Scholar 

  22. H. Rudin, “Validation of a token-ring protocol,” in Proc. Intl. Symposium on Local Computer Networks, Florence, April, 1982, (North-Holland, Amsterdam, 1982) pp. 373–387.

    Google Scholar 

  23. H. Rudin, “From formal protocol specification towards automated performance prediction,” Proc. Workshop on Protocol Specification, Testing, and Verification, III, Rüschlikon, Switzerland, May 1983, (North-Holland, Amsterdam, 1983) pp. 257–269.

    Google Scholar 

  24. H. Rudin, “An improved algorithm for estimating protocol performance,” Proc. Workshop on Protocol Specification, Testing, and Verification, IV, Sky Top, Pennsylvania, June 1984, (North-Holland, Amsterdam, 1984).

    Google Scholar 

  25. H. Rudin, “An informal overview of formal protocol specification,” IEEE Communications Magazine, probably February, 1985.

    Google Scholar 

  26. J. Sifakis, “Performance evaluation using nets,” Net Theory and Applications, Lecture Notes in Computer Science No. 84, (Springer Verlag, Heidelberg, 1979), pp. 307–319.

    Google Scholar 

  27. F. J. W. Symons, “Modeling and analysis of communication protocols using numerical Petri nets,” Ph.D. Thesis at University of Essex, England, May, 1978.

    Google Scholar 

  28. C. A. Vissers, R. L. Tenney, and G. V. Bochmann, “Formal Description Techniques,” Special issue on OSI, Proc. IEEE, Vol. 71, No. 12, December, 1983, pp. 1356–1364.

    Google Scholar 

  29. B. Walter, “Timed Petri-nets for modelling and analyzing protocols with real-time characteristics,” Proc. Workshop on Protocol Specification, Testing, and Verification, III, Rüschlikon, Switzerland, May 1983, (North-Holland, Amsterdam, 1983) pp. 149–159.

    Google Scholar 

  30. C.H. West, “General technique for communications protocol validation,” IBM J. Res. Develop., Vol. 22, July 1978, pp. 393–404.

    Article  Google Scholar 

  31. C. Y. Wong, T. S. Dillon, and K. E. Forward, “Analysis of timing aspects of communication computer systems using timed places Petri nets,” Proc. Seventh International Conference on Computer Communication, Sydney, October 30 -November 2, 1984, pp. 585–590.

    Google Scholar 

  32. P. Zafiropulo, “Protocol validation by duologue-matrix analysis,” IEEE Trans. Commun., Vol. COM-26, Aug. 1978, pp. 1187–1194.

    Article  Google Scholar 

  33. W. M. Zuberek, “Timed Petri nets and preliminary performance evaluation,” Proc. 7th Annual IEEE Symposium on Computer Architecture, 1980, pp. 88–96.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rudin, H. (1985). Time in Formal Protocol Specifications. In: Heger, D., Krüger, G., Spaniol, O., Zorn, W. (eds) Kommunikation in Verteilten Systemen I. Informatik-Fachberichte, vol 95. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-70285-3_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-70285-3_35

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-15197-5

  • Online ISBN: 978-3-642-70285-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics