Two Exercises with EMPA: Computing the Utilization of the CSMA/CD Protocol and Assessing the Performability of a Queueing System

We present two applications of the stochastically timed process algebra EMPA. The first one is concerned with the compositional modeling of the CSMA/CD protocol and the determination of its utilization. The second one is concerned with the description of a queueing system representing a computing center where failures and repairs can occur, and the compositional assessment of its performability. In both cases, the technique of rewards is used to determine performance measures. 1 Compositional performance modeling The need of integrating the performance modeling and analysis of a concurrent system into the design process of the system itself has been widely recognized (see, e.g., [27, 7, 12, 4]) and stimulated a considerable research effort. The main problem to be tackled is that it often happens that a concurrent system is first fully designed and tested for functionality, and afterwards tested for efficiency. As a consequence, if the performance is detected to be poor, the concurrent system has to be designed again, thereby negatively affecting both the design costs and the delivery at a fixed deadline. Another relevant drawback is that tests for functionality and performance are usually carried out on two different models of the system, so one has to make sure that the functional model and the performance model are consistent, i.e. they really describe (different aspect