Stochastic Process Algebras for the Analysis of Internet Protocols

In the last decade a new formal approach to the integration of performance aspects in the modeling and analysis of concurrent systems has emerged with Stochastic Process Algebras (SPAs for short). Like classical process algebras, they are algebraic languages endowed with a small set of powerful operators whereby it is possible to construct algebraic models from simpler ones. The main advantages of this approach are summarized with the motto: integration and compositionality (see e.g. [2]). There are several forms of integration supported by SPAs, including those illustrated below: – functionality and performance: both aspects are to be described in the unique specification model, called integrated model. This has the advantage of en-suring coherence of the functional and performance (sub-)models as they both originate by projection from the same integrated model. Moreover, the integrated model is justified also because it allows the analysis of mixed properties (e.g., mean time to deadlock) and makes easier proof of functional properties for which the probabilistic aspect may be relevant