Specification and verification of real-time broadcast networks
Pradeep Jain · 1991
A real time communications protocol satisfies certain timing constraints in order to meet its service specification. A new generation of real-time protocols has been proposed for broadcast bus networks that operate at very high speeds (50-200 Mbps). These protocols exploit the directionality of signal propagation and impose stringent timing constraints to provide collision-free access to a shared bus within a bounded delay. These features make these protocols particularly suitable for real-time applications, such as the transport of integrated data, voice, video and facsimile traffic. The behavior of a typical real-time protocol is complex and, to have reasonable confidence in its implementation, it has to be analyzed using a formal method. Although a number of real-time protocols for broadcast bus networks have been proposed, there is no formal method for their analyses. We present a model for specifying and verifying real-time protocols for high-speed broadcast bus networks. In this model, the network topology and broadcast bus behavior is specified by a set of channel axioms that model the actual propagation of signals with time along the bus. Protocol entities are specified as sequential programs in a Pascal-like specification language that includes two novel wait constructs. The interaction between channels and protocol entities is modeled by shared variables. Real time is modeled by a global clock, time variables and a time event. A first-order logic, that includes time variables, is used to reason about the temporal behavior of the protocol. To illustrate our model and verification method, we specify two protocols proposed in the literature, the EHS protocol and the Expressnet protocol. The topology of the EHS protocol consists of a bidirectional broadcast bus and a unidirectional control wire. We prove that the protocol is collision-free using an assertional proof method. The topology of the Expressnet protocol consists of a folded unidirectional bus. We apply a proof method based on timed-reachability analysis to the Expressnet protocol. Our analysis shows that the original Expressnet protocol is not collision-free. To achieve collision-freedom, we propose a modification to the protocol. We show that the modified protocol is collision-free and also derive a bound for the access delay.