The Modelling and Analysis of a High Speed Data Bus with Predicate/Transition Nets

Reference:

Tino Pyssysalo. The modelling and analysis of a high speed data bus with predicate/transition nets. Research Report A29, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland, March 1994.

Abstract:

In this work predicate/transition nets (Pr/T-nets) are used in the modelling and analysis of the medium access control algorithm of a parallel high speed data bus, Frame Synchronized Ring (FSR-bus). Two Pr/T-net models of the bus are presented. One models the basic operation of the control algorithm. The other is an extended model, in which nodes can send longer frames and the reception of a frame can fail. The analysis of the nets is based on the reachability analysis, which is made by a highly advanced Pr/T-net reachability analysis tool, PROD. The state space of the reachability graph grows very fast with respect to the number of nodes in the ring. The state space explosion is tried to be reduced with the stubborn set and symmetry methods. The stubborn set method reduces the number of reachable states almost 70%. Symmetry method is not so efficient. These results show, how effective these methods can be. Analytical models and simulations have been used in the analysis of the FSR-bus. With these methods it has not been possible to prove, whether the bus can deadlock or whether the bus is fair. In this work these properties are successfully proved with PROD. Other important results concern the performance of the FSR-bus in terms of waiting times of the nodes. The longest waiting path and the situation, in which the waiting occurs, are examined with PROD. It is found that in some circumstances a node has to wait quite long to get access to the bus, which is undesirable in real time applications.

Keywords:

concurrent and distributed systems, protocol verification, predicate/transition nets, reachability analysis tools, Frame Synchronized Ring

Suggested BibTeX entry:

@techreport{HUT-TCS-A29,
    address = {Espoo, Finland},
    author = {Tino Pyssysalo},
    institution = {Helsinki University of Technology, Digital Systems Laboratory},
    month = {March},
    number = {A29},
    pages = {73},
    title = {The Modelling and Analysis of a High Speed Data Bus with Predicate/Transition Nets},
    type = {Research Report},
    year = {1994},
}