Premium
Estimating protocol performance using a formal specification model
Author(s) -
Miller Raymond E.,
Chaudhry Zafar Ullah
Publication year - 1999
Publication title -
international journal of communication systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.344
H-Index - 49
eISSN - 1099-1131
pISSN - 1074-5351
DOI - 10.1002/(sici)1099-1131(199909/12)12:5/6<325::aid-dac414>3.0.co;2-u
Subject(s) - computer science , reachability , protocol (science) , formal methods , formal specification , model checking , distributed computing , programming language , theoretical computer science , medicine , alternative medicine , pathology
This paper introduces an approach for protocol performance estimation directly from a formal model of the protocol. By using the approach presented in this paper, performance of a protocol can be quickly estimated at an early stage of protocol design. The simplicity of analysis, achieved by deterministic analysis, and the tight integration of the performance model, called the performance reachability graph (PRG), with the formal specification makes the approach in this paper a very useful protocol design‐time tool. The approach provides a two‐way path between the specification model and the performance model. In one direction, the tight coupling between the specification and the performance models allows a protocol designer to get quick estimates of performance from the specification. In the other direction a designer can use the performance estimates to quickly identify portions of the specification responsible for undesired performance characteristics and consider changes to the specification to improve the overall performance. Copyright © 1999 John Wiley & Sons, Ltd.