Estimating performance of communication protocols from formal specifications

This thesis introduces an approach for integrating performance estimation of a protocol with formal model of the protocol. By using the approach presented in this thesis, performance of a protocol can be quickly estimated at an early stage during protocol design. The simplicity of analysis, achieved by deterministic analysis, and the tight integration of the performance model with the specification makes the approach in this thesis a very useful protocol design tool. The approach provides a two way path between the specification model and the performance model. In one direction, the tight coupling between specification and the performance models allows a protocol designer to get quick estimates of the protocols' performance from its specification and in the other direction, the designer can use the performance model to quickly identify portions of the specification responsible for causing low performance.;The usefulness of the approach presented in this thesis can be evaluated by comparing it with the existing stochastic performance analysis techniques. For the stochastic analysis approach to be applied to a protocol, one needs to assume particular load distributions on the information to be transmitted. On the other hand, the approach developed in this thesis enables one to find performance equations directly from the protocol specification. Furthermore, in most of the cases, complexity of the stochastic analysis approach hides the basic protocol specification parameters, thereby making it difficult to identify the specification parameters from the stochastic performance model that are responsible for undesirable protocol behavior. Since the approach in this thesis derives the performance model directly from the specification, there is a tight coupling between protocol performance variables and the basic specification variables. Additionally, the amount of effort involved in stochastic analysis of a protocol makes the stochastic approach more appropriate as a post-design performance tool rather than a design-time tool. In contrast, the use of deterministic analysis in this thesis provides; much quicker performance estimates, a feature highly desired during protocol design phase. It should be noted here that the approach presented in this thesis complements the stochastic approach. Once a protocol's design is finalized, the stochastic approach can be used for detailed studies of the protocol.;Since, most of the modeling work has been done at the media access layer, the techniques in this thesis are demonstrated by applying them to Media Access Protocols (MAC). The work in this thesis can be extended further by applying the techniques presented here towards upper layer protocols. Further extensions can be made by studying the interaction between protocols within the same protocol stack.