Proving properties of a new high speed data bus with predicate/transition nets

Frame Synchronized Ring (FSR-bus) is a new high speed interconnection network, developed for a wide range of real time applications. The medium access control (MAC) algorithm of the FSR has been analyzed with analytical models and simulations. However, these methods have not been powerful enough for proving some interesting properties of the algorithm. In this paper we explain, how predicate/transition (Pr/T) nets can be used in the modeling of the FSR-bus. In addition, we prove the deadlock freeness and the fairness of the MAC by analyzing the Pr/T-net model of the FSR.