Evaluating performance from formal specification

This paper proposes a new methodology for integrating performance evaluation and formal specification. This methodology intends to reuse the formal specification effort to create a performance modeling. Our idea is to start abstracting the relevant features of the real system in the formal specification. Then, we enhance the specification with information for performance modeling (quality of service, workload, processing design and processing constraints). At that point, we map the enhanced formal representation in a performance modeling that maintains the formal properties. Next, we implement this modeling in a performance evaluation environment. Finally, we run simulations of the achieved executable varying evaluation conditions. Our methodology is applied to the Specification and Description Language (SDL). Ultimately, we explain the methodology through an example: the Transport Control Protocol (TCP)