Several stochastic extensions of process algebras (SPAs) have been proposed to describe and analyze both functional and performance properties and quality of service (QoS) evaluation. Among these, we consider time processes and performability evaluation (TIPP), extended Markovian process algebra (EMPA), and performance evaluation process algebra (PEPA), all of which are supported by appropriate tools (the TIPP tool, PEPA Workbench, and TwoTowers for EMPA). This last tool is used in this paper to design, verify, simulate, and implement Internet protocol (IP) audio mechanisms.

The advantage of using EMPA for analysis and simulation is that it supports the integration of functional and nonfunctional aspects, and provides a unique reference model for model specification and performance. However, from the performance evaluation viewpoint, the analysis usually refers to the numerical solution of the underlying Markov chain, which can easily lead to numerical problems due to the state space explosion. On the designer’s side, the analyst is required to be able to specify the audio system using process algebras, and to associate the appropriate performance parameters (namely, activity rates) with actions. Further development of tools, such as Emilia, seeks to facilitate the work of the designer in the process algebra-based specification of architectures, by means of syntactic constructs. Moreover, for Emilia specifications, a translation into QN models has been proposed, in order to take advantage of the orthogonal strengths of the two formalisms: formal techniques for the verification of functional properties for Emilia (SPA in general), and efficient performance analysis for QN.