Functional and Performance Modeling and Analysis of Token Ring using EMPA

We present an application of the integrated approach based on the stochastically timed process algebra EMPA to the analysis of token ring. The protocol is formally represented in EMPA. The deadlock freeness of the protocol and the utilization of the channel are then assessed by automatically analyzing the algebraic description with the EMPA based software tool TwoTowers. Finally, we show the potentialities of the integrated approach by investigating the fairness of the protocol, which depends on both functional and performance aspects. 1 A Formal Approach to Performance Evaluation Assessing the performance of a system is an important activity which has to be carried out during the development of the system itself. The desirability of taking into account the performance aspects of a system in the early stages of its design has been widely recognized 12,6. Nevertheless, it often happens that a concurrent system is tested for efficiency only after it has been fully designed and tested for functionality. This results in two problems. On the one hand, the detection of poor performance causes the system to be designed again, s