An approach to evaluating the performance of communications protocols based on formal specifications

This paper proposes an approach to modeling and evaluating the performance of communications protocols based on formal specifications. A combined Extended Finite State Machine (EFSM) and Queueing Network (QN) model is presented which is more sophisticated than either technique alone. Furthermore, the model avoids the state space explosion problem which may arise by the use of reachability analysis on EFSM. The approach is illustrated using a simple sliding window protocol written in the formal description technique Estelle