Issue No. 04 - April (1991 vol. 40)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.88461
<p>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.</p>
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.
P. Jain and S. Lam, "Specification of Real-Time Broadcast Networks," in IEEE Transactions on Computers, vol. 40, no. , pp. 404-422, 1991.