Timed Ethernet: Real-time formal specification of Ethernet

  • Henri B. Weinberg
  • Lenore D. Zuck
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


The goal of this paper is to show how formal specification can be applied to a full-fledged, real-world protocol while maintaining, or even enhancing, readability. The system we formally specify is Ethernet as it appears in IEEE 802.3. We focus on the specification of the Medium Access Control (MAC) layer—the part of the Data Link Layer that implements a 1-persistent CSMA/CD protocol — and its interfaces with adjacent layers. The specification method is based on one of Henzinger's real-time models. We believe that the readability of our specification is due to the graphical presentation using transition graphs of real-time programs.


Medium Access Control Temporal Logic Physical Layer Message Passing Transition Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford University, August 1991.Google Scholar
  2. 2.
    D. Bertsekas and R. Gallager. Data Networks. Prentice-Hall, 1987.Google Scholar
  3. 3.
    G. V. Bochmann and J. Gecsei. A unified method for the specification and verification of protocols. In B. Gilchrist, editor, Information Processing 77, pages 229–234, Amsterdam, 1977. North-Holland Publishing Co.Google Scholar
  4. 4.
    G. V. Bochmann and C. A. Sunshine. Formal methods in communication protocol design. IEEE Transactions on Communications, COM-28:624–631, 1980.CrossRefGoogle Scholar
  5. 5.
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 8(2):244–263, 1986. An early version appeared in Proceedings of the 10th ACM Symposium on Principles of Programming Languages, 1983.zbMATHCrossRefGoogle Scholar
  6. 6.
    J. D. Day and H. Zimmerman. The OSI reference model. In Proc. of IEEE, volume 71, pages 1334–1340, December 1983.CrossRefGoogle Scholar
  7. 7.
    D. Dill. Timing assumption and verification of finite-state concurrent system. In J. Sifakis, editor, Automatic Verification MEthods for Finite State Systems, LNCS 407. Springer-Verlag, 1989.Google Scholar
  8. 8.
    Michael Fischer and Lenore Zuck, August 1991. Preliminary work on spcification of CSMA/CD protocols.Google Scholar
  9. 9.
    V. D. Gligor and S. H. Shattuck. On deadlock detection in distributed systems. IEEE Transactions on Software Engineering, SE-6(5):435–440, 1980.Google Scholar
  10. 10.
    B. T. Hailpern and S. S. Owicki. Modular verification of communication protocols. IEEE Transactions on Communications, COM-31(1):56–68, 1983.CrossRefGoogle Scholar
  11. 11.
    J. L. Hammonds and P. J. P. O'Reilly. Performance Analysis of Local Computer Networks. Addison-Wesley, 1986.Google Scholar
  12. 12.
    D. Harel. Statecharts: A visual formalism for complex systesm. Sci. COmp. Prog., 8:231–274, 1987.zbMATHMathSciNetCrossRefGoogle Scholar
  13. 13.
    J. F. Hayes. Modeling and Analysis of Computer Communication Networks. Plenum Press, 1984.Google Scholar
  14. 14.
    T. A. Henzinger. The Temporal Specification and Verification of Real-Time Systems. PhD thesis, Stanford University, August 1991.Google Scholar
  15. 15.
    T. A. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for real-time systems. In Proc. of 18th POPL, pages 353–366, 1991.Google Scholar
  16. 16.
    H. R. Lewis. Finiste-state analysis of asynchrocous circuits with bounded temporal uncertainty. Technical Report TR-15-89, Haravard University, 1989.Google Scholar
  17. 17.
    N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 137–151, August 1987.Google Scholar
  18. 18.
    Z. Manna and A. Pnueli. The anchor version of the temporal framework. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching time, and Parital Order Models and Logics for Concurrency, pages 201–284. Springer Verlag, LNCS 354, 1989.Google Scholar
  19. 19.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems (Specification). Springer-Verlag, 1992.Google Scholar
  20. 20.
    P. M. Merlin. A methodology for the design and implementation of communication protocols. IEEE Transactions on Communications, COM-24(4):614–621, 1976.MathSciNetCrossRefGoogle Scholar
  21. 21.
    M. Merritt, F. Modugno, and M. Tuttle. Time constrained automata. Manuscript, August 1990.Google Scholar
  22. 22.
    R. M. Metcalfe and D. R. Boggs. Ethernet: Distributed packet swithching for local computer networks. Communications of the ACM, 19:395–404, July 76.Google Scholar
  23. 23.
    F. Moller and C. Tofts. A temporal calculus of communicating processes. In J. C. M. Baeton and J. W. Klop, editors, CONCUR 90, LNCS 458, pages 401–415. Springer-Verlag, 1990.Google Scholar
  24. 24.
    J. Orsroff. Temporal Logic of Real Time Systems. Research Studies Press, 1990.Google Scholar
  25. 25.
    S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. on Programming Languages and Systems, 4(3):455–495, 1982.zbMATHCrossRefGoogle Scholar
  26. 26.
    A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foundations of Computer Science, pages 46–57, 1977.Google Scholar
  27. 27.
    J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int'l Symp. on Programming, 1981.Google Scholar
  28. 28.
    G. M. Reed and A. W. Roscoe. A timed model for communicating sequential processes. Theoretical Computer Science, 58:249–26, 1988.zbMATHMathSciNetCrossRefGoogle Scholar
  29. 29.
    R. L. Schwartz and P. M. Melliar-Smith. From state machines to temporal logic: Specification methods for protocol standards. IEEE Transactions on Communications, 1982.Google Scholar
  30. 30.
    S. R. Soloway and P. A. Humblet. On distributed network protocols for changing topologies. Technical Report LIDS-P-1564, MIT, 1986.Google Scholar
  31. 31.
    ANSI/IEEE std. Information Processing Systems-Local Area Networks-Part 3: Carrier sense multiple access with collision detection (CSMA/CD) access method and physical layer specificaitons. The IEEE, Inc., NY, October 1991.Google Scholar
  32. 32.
    C. A. Sunshine. Formal techniques for protocol specification and verification. IEEE Computer, 12:20–27, 1979.Google Scholar
  33. 33.
    A. Tanenbaum. Computer Networks. Prentice Hall, 2nd edition, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Henri B. Weinberg
    • 1
  • Lenore D. Zuck
    • 1
  1. 1.Department of Computer ScienceYale UniversityUSA

Personalised recommendations