Specification and verification of collusion-free broadcast networks
P. Jain, Simon S. Lam · 1988
For high-speed local area networks that offer integrated services for data, voice, and image traffic, a class of demand-assigned multiple-access protocols have been presented in the literature. These protocols exploit the directionality of signal propagation and enforce time constraints to achieve collision-freedom. A correct implementation of such a protocol requires a careful analysis of time-dependent interactions of event occurrences using a formal method. To date, most protocol verification methods are intended for the analysis of asynchronous communication over point-to-point channels.