SPECIFICATION OF REAL-TIME BROADCAST NETWORKS

We 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 our model by a set of channel axioms. Protocol entities are specified by sequential programs. The semantics of a set of programming constructs, including two novel wait constructs, are defined. To illustrate our model and verification method, we present a specification of the Expressnet protocol which was designed for collision-free access to a unidirectional bus. We discovered a scenario in which collisions can occur in the original Expressnet. To guarantee collision-freedom, we provide a modification to the protocol. The modified protocol is shown to be collision-free. We also derive a bound for its access delay.