This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Specification of Real-Time Broadcast Networks
April 1991 (vol. 40 no. 4)
pp. 404-422

The authors present a model for specifying real-time protocols that execute on broadcast bus networks. Protocol entities interact by sending and receiving binary signals on buses. The actual propagation of these signals is captured in the proposed model by a set of channel axioms. Protocol entities are specified by sequential programs. The semantics of a set of programming constructs, including two level wait constructs, are defined. To illustrate the model and verification method, the authors present a specification of the Expressnet protocol which was designed for collision-free access to a unidirectional bus. A scenario in which collisions can occur in the original Expressnet was discovered. To guarantee collision-freedom, a modification to the protocol is given. The modified protocol is shown to be collision-free. A bound for its access delay is also derived.

[1] G. v. Bochmann, "Finite state description of communication protocols,"Comput. Networks, vol. 2, pp. 361-372, Oct. 1978.
[2] E. W. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs,"Commun. ACM, vol. 18, no. 8, pp. 453- 457, 1975.
[3] K. Eswaran, V. C. Hamacher, and G. S. Shedler, "Collision-free access control for communication bus networks,"IEEE Trans. Software Eng., vol. SE-7, pp. 574-582, Nov. 1981.
[4] M. Fine and F. Tobagi, "Demand assignment multiple access schemes in broadcast-bus local area networks,"IEEE Trans. Comput., vol. C-33, pp. 1130-1159, Dec. 1984.
[5] L. Fratta, "An improved access protocol for data communication bus networks with control wire," inProc ACM SIGCOMM Symp., Austin, TX, Mar. 1983.
[6] M. Gouda, "Closed covers: To verify progress of communicating finite state machines,"IEEE Trans. Software Eng., vol. SE-10, pp. 846-855, Nov. 1984.
[7] B. Hailpern and S. Owicki, "Modular verification of computer communication protocols,"IEEE Trans. Comm., vol. COM-31, Jan. 1983.
[8] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[9] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[10] P. Jain and S. S. Lam, "Modeling and verification of real-time protocols for broadcast networks,"IEEE Trans. Software Eng., vol. SE-13, pp. 924-937, Aug. 1987.
[11] P. Jain, "Specification and verification of real-time broadcast networks," Ph.D. dissertation, Dep. Comput. Sci., Univ. of Texas at Austin, 1991.
[12] S. S. Lam and A. U. Shankar, "Protocol verification via projections,"IEEE Trans. Software Eng., vol. SE-10, pp. 325-342, July 1984.
[13] S. S. Lam and A. U. Shankar, "A relational notation for state transition systems,"IEEE Trans. Software Eng., vol. 16, no. 7, pp. 755-775, July 1990.
[14] G. M. Lundy and R. E. Miller, "A variable window protocol specification and analysis," inProc. 8th Int. Symp. Protocol Specification, Testing, Verification, Atlantic City, NJ, June 1988.
[15] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE-7, pp. 417-426, July 1981.
[16] Owicki, S., and L. Lamport, "Proving Liveness Properties of Concurrent Programs,"ACM Trans. Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 455-495.
[17] A. U. Shankar and S. S. Lam, "An HDLC protocol specification and its verification using image protocols,"ACM Trans. Comput. Syst., vol. 1, no. 4, pp. 321-368, Nov. 1983.
[18] A. U. Shankar and S. S. Lam, "Time-dependent distributed systems: proving safety, liveness and real-time properties,"Distributed Compu., vol. 2, pp. 61-79, 1987.
[19] F. A. Tobagi, F. Borgonovo, and L. Fratta, "EXPRESS-NET: A high performance integrated services local area network,"IEEE J. Select. Areas Commun., vol. SAC-1, no. 5, pp. 898-913, Nov. 1983.
[20] C. Tseng and B. Chen, "D-Net, A New Scheme for High Data Rate Optical Local Area Networks,"IEEE J. Selected Areas Comm., Vol. SAC-1, Apr. 1983, pp. 495-499.
[21] P. Zafiropouloet al., "Towards analysing and synthesizing protocols,"IEEE Trans. Commun., vol. COM-28, pp. 655-660, Apr. 1980.

Index Terms:
protocols specification; real-time broadcast networks; model; broadcast bus networks; binary signals; sequential programs; programming constructs; two level wait constructs; Expressnet protocol; collision-free access; access delay; computer networks; formal specification; protocols; real-time systems.
Citation:
P. Jain, S.S. Lam, "Specification of Real-Time Broadcast Networks," IEEE Transactions on Computers, vol. 40, no. 4, pp. 404-422, April 1991, doi:10.1109/12.88461
Usage of this product signifies your acceptance of the Terms of Use.