Analyzing Performance for Complex Protocol using Validated CP-nets Models

Performance improvements are quite significant for a complex protocol, such as BitTorrent protocol, but should take no harm to its functionality correctness as an inevitable precondition. In current performance analysis studies, various formal models are usually utilized to perform corresponding evaluations. However, most of those models do not support specifying and verifying the functionality for protocol systems, where above precondition may not be guaranteed before performance analysis executes. Therefore, how to analysis performance for complex protocols based on functional validated models becomes a challenging but significant topic. In this paper, colored Petri nets (CP-nets) is well utilized as basic models to integrate functional validation and performance analysis for complex protocols. The CP-nets models used in functional validation and performance analysis procedures are closely related, where every occurrence sequence in the performance model corresponds to a behavioral equivalent occurrence sequence in its functional model, so it is guaranteed that models used in performance analysis also satisfy the functionality requirements of the protocol. An integrated analysis process of BitTorrent protocol is taken as an example to illustrate the practical effectiveness of our method.