Abstract
In this tutorial we give an introduction to stochastic process algebras and their use in performance modelling, with a focus on the PEPA formalism. A brief introduction is given to the motivations for extending classical process algebra with stochastic times and probabilistic choice. We then present an introduction to the modelling capabilities of the formalism and the tools available to support Markovian based analysis. The chapter is illustrated throughout by small examples, demonstrating the use of the formalism and the tools.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Label Transition System
- Process Algebra
- Communicate Sequential Process
- Derivation Graph
- Steady State Probability Distribution
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Herzog, U.: Formal description, time and performance analysis: A framework. Technical Report 15/90, IMMD VII, Friedrich-Alexander-Universität, Erlangen-Nürnberg, Germany (September 1990)
Holton, D.: A PEPA specification of an industrial production cell. The Computer Journal (Special Issue: Gilmore, S., Hillston, J., eds.: Proceedings of the Third International Workshop on Process Algebras and Performance Modelling) 38(7), 542–551 (1995)
Gilmore, S., Hillston, J., Holton, D.R.W., Rettelbach, M.: Specifications in Stochastic Process Algebra for a Robot Control Problem. International Journal of Production Research 34(4), 1065–1080 (1996)
Thomas, N., Hillston, J.: Using Markovian process algebra to specify interactions in queueing systems. Technical Report ECS-LFCS-97-373, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh (1997)
Bowman, H., Bryans, J., Derrick, J.: Analysis of a multimedia stream using stochastic process algebra. In: Priami, C. (ed.) Sixth International Workshop on Process Algebras and Performance Modelling, Nice, September 1998, pp. 51–69 (1998), http://www.cs.ukc.ac.uk/pubs/1998/611
Console, L., Picardi, C., Ribaudo, M.: Diagnosis and Diagnosability Analysis using PEPA. In: Proc. of 14th European Conference on Artificial Intelligence, Berlin (August 2000), A longer version appeared in the Proc. of 11th Int. Workshop on Principles of Diagnosis (DX00), Morelia, Mexico (June 2000)
Hillston, J., Kloul, L.: Performance investigation of an on-line auction system. Concurrency and Computation: Practice and Experience 13, 23–41 (2001)
Forneau, J.M., Kloul, L., Valois, F.: Performance modelling of hierarchical cellular networks using PEPA. Performance Evaluation 50(2-3), 83–99 (2002)
Brodo, L., Degano, P., Gilmore, S., Hillston, J., Priami, C.: Performance evaluation for global computation. In: Priami, C. (ed.) GC 2003. LNCS, vol. 2874, pp. 229–253. Springer, Heidelberg (2003)
Buchholtz, M., Gilmore, S., Hillston, J., Nielson, F.: Securing statically-verified communications protocols against timing attacks. Electr. Notes Theor. Comput. Sci. 128(4), 123–143 (2005)
Hillston, J., Kloul, L., Mokhtari, A.: Towards a feasible active networking scenario. Telecommunication Systems 27(2-4), 413–438 (2004)
Fourneau, J.-M., Kloul, L.: A Precedence PEPA Model for Performance and Reliability Analysis. In: Horváth, A., Telek, M. (eds.) EPEW 2006. LNCS, vol. 4054, pp. 1–15. Springer, Heidelberg (2006)
Duguid, A.: Coping with the Parallelism of BitTorrent: Conversion of PEPA to ODEs in Dealing with State Space Explosion. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 156–170. Springer, Heidelberg (2006)
Gilmore, S., Tribastone, M.: Evaluating the Scalability of a Web Service-Based Distributed e-Learning and Course Management System. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 214–226. Springer, Heidelberg (2006)
Razafindralambo, T., Valois, F.: Performance evaluation of backoff algorithms in 802.11 ad-hoc networks. In: PE-WASUN ’06: Proceedings of the 3rd ACM international workshop on Performance evaluation of wireless ad hoc, sensor and ubiquitous networks, Terromolinos, Spain, pp. 82–89. ACM Press, New York (2006)
Razafindralambo, T., Valois, F.: Stochastic behavior study of backoff algorithms in case of hidden terminals. In: Proceedings of the 17th Annual IEEE International Symposium on Personal, Indoor and Mobile Radio Communications (PIMRC’06), Helsinki, Finland, pp. 1–6. IEEE Computer Society Press, Los Alamitos (2006)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Nicollin, X., Sifakis, J.: An Overview and Synthesis on Timed Process Algebras. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) Real-Time: Theory in Practice. LNCS, vol. 600, pp. 526–548. Springer, Heidelberg (1992)
Moller, F., Tofts, C.: A Temporal Calculus for Communicating Systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401–415. Springer, Heidelberg (1990)
Jou, C.-C., Smolka, S.A.: Equivalences, Congruences and Complete Axiomatizations of Probabilistic Processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 367–383. Springer, Heidelberg (1990)
Edinburgh Concurrency Workbench. http://homepages.inf.ed.ac.uk/perdita/cwb/
Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27(3), 333–354 (1983)
Götz, N., Herzog, U., Rettelbach, M.: TIPP—a language for timed processes and performance evaluation. Technical Report 4/92, IMMD7, University of Erlangen-Nürnberg, Germany (November 1992)
Bernardo, M., Gorrieri, R., Donatiello, L.: MPA: A Stochastic Process Algebra. Technical Report UBLCS-94-10, Laboratory of Computer Science, University of Bologna (May 1994)
Bernardo, M., Gorrieri, R.: A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Theoretical Computer Science, to appear (1998)
Hillston, J.: PEPA - Performance Enhanced Process Algebra. Technical report, Dept. of Computer Science, University of Edinburgh (March 1993)
Hillston, J.: A Compositional Approach to Performance Modelling. PhD thesis, CST-107-94, Department of Computer Science, University of Edinburgh (April 1994)
Strulo, B.: Process Algebra for Discrete Event Simulation. PhD thesis, Imperial College (1993)
Priami, C.: Stochastic π-Calculus. The Computer Journal 38(6) (1995)
Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
D’Argenio, P.R., Hermanns, H., Katoen, J.-P., Klaren, R.: MoDeST - A Modelling and Description Language for Stochastic Timed Systems. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 87–104. Springer, Heidelberg (2001)
Bravetti, M., Gorrieri, R.: The theory of Interactive Generalized Semi-Markov Processes. Theoretical Computer Science 282(1), 5–32 (2002)
Bravetti, M., Bernardo, M., Gorrieri, R.: From EMPA to GSMPA: Allowing for general distributions. In: Brinksma, E., Nymeyer, A. (eds.) Proc. of the 5th Int. Workshop on Process Algebras and Performance Modeling (PAPM ’97), pp. 17–33 (1997)
Rettelbach, M.: Probabilistic Branching in Markovian Process Algebras. The Computer Journal (Special Issue: Proc. of 3rd Process Algebra and Performance Modelling Workshop) 38(6) (1995)
Hermanns, H., Rettelbach, M., Weiß, T.: Formal Characterisation of Immediate Actions in SPA with Nondeterministic Branching. The Computer Journal (Special Issue: Proc. of 3rd Workshop on Process Algebras and Performance Modelling) 38(6) (1995)
Hillston, J.: The nature of synchronisation. In: Herzog, U., Rettelbach, M. (eds.) Proceedings of the Second International Workshop on Process Algebras and Performance Modelling, Erlangen, November 1994, pp. 51–70 (1994)
Ribaudo, M.: Understanding Stochastic Process Algebras via their Stochastic Petri Net Semantics. In: Herzog, U., Rettelbach, M. (eds.) Proc. of 2nd Process Algebra and Performance Modelling Workshop (1994)
Bradley, J.: Towards Reliable Modelling with Stochastic Process Algebras. PhD thesis, Department of Computer Science, University of Bristol (1999)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Clark, G., Gilmore, S., Hillston, J., Ribaudo, M.: Exploiting Modal Logic to Express Performance Measures. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds.) TOOLS 2000. LNCS, vol. 1786, pp. 211–227. Springer, Heidelberg (2000)
Dempster, E.W., Tomov, N.T., Lü, J., Pua, C.S., Williams, M.H., Burger, A., Taylor, H., Broughton, P.: Verifying a Performance Estimator for Parallel DBMSs. In: Pritchard, D., Reeve, J.S. (eds.) Euro-Par 1998. LNCS, vol. 1470, p. 126. Springer, Heidelberg (1998)
Bouzeghoub, M., Kloul, L., Mokhtari, A.: A new active network framework based on active rules. Technical Report 2002/21, PRiSM, Université de Versailles (2002)
Hillston, J., Kloul, L., Mokhtari, A.: Active nodes performance analysis using PEPA. In: Jarvis, S. (ed.) Proceedings of the Ninteenth UK Performance Engineering Workshop, University of Warwick, July 2003, pp. 244–256 (2003)
Hillston, J., Kloul, L., Mokhtari, A.: Towards a feasible active networking scenario. Telecommunication Systems 27(2-4), 413–438 (2004)
Gilmore, S., Hillston, J., Ribaudo, M.: An efficient algorithm for aggregating PEPA models. IEEE Transactions on Software Engineering 27(5), 449–464 (2001)
Console, L., Picardi, C., Ribaudo, M.: Diagnosis and Diagnosability Analysis using Process Algebras. In: Proc. of 11th Int. Workshop on Principles of Diagnosis (DX00), Morelia, Mexico (June 2000)
Eclipse.org home, http://www.eclipse.org
Eclipse Modeling Framework, http://www.eclipse.org/home
Matrix Toolkit for Java, http://rs.cipr.uib.no/mtj/
Bradley, J.T., Dingle, N.J., Gilmore, S.T., Knottenbelt, W.J.: Derivation of passage-time densities in PEPA models using IPC: The Imperial PEPA Compiler. In: Kotsis, G. (ed.) Proceedings of the 11th IEEE/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunications Systems, University of Central Florida, Oct. 2003, pp. 344–351. IEEE Computer Society Press, Los Alamitos (2003)
Knottenbelt, W.: Generalised Markovian analysis of timed transition systems. Master’s thesis, University of Cape Town (1996)
Bradley, J., Dingle, N., Gilmore, S., Knottenbelt, W.: Extracting passage times from PEPA models with the HYDRA tool: A case study. In: Jarvis, S. (ed.) Proceedings of the Ninteenth UK Performance Engineering Workshop, University of Warwick, July 2003, pp. 79–90 (2003)
Argent-Katwala, A., Bradley, J.T., Dingle, N.J.: Expressing performance requirements using regular expressions to specify stochastic probes over process algebra models. In: Proceedings of the Fourth International Workshop on Software and Performance, Redwood Shores, California, USA, Jan. 2004, pp. 49–58. ACM Press, New York (2004)
Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi-terminal binary decision diagrams to represent and analyse continuous time markov chains. In: Proc. of 3rd Intl. Workshop on the Numerical Solution of Markov Chains, pp. 188–207 (1999)
Gilmore, S., Kloul, L.: A Unified Tool for Performance Modelling and Prediction. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 179–192. Springer, Heidelberg (2003)
Gilmore, S., Hillston, J., Kloul, L., Ribaudo, M.: Software performance modelling using PEPA nets. In: Proceedings of the Fourth International Workshop on Software and Performance, Redwood Shores, California, USA, Jan. 2004, pp. 13–24. ACM Press, New York (2004)
Clark, G., Courtney, T., Daly, D., Deavours, D., Derisavi, S., Doyle, J.M., Sanders, W.H., Webster, P.: The Möbius modeling tool. In: Proc. of 9th Int. Workshop on Petri Nets and Performance Models, Aachen, Germany, Sep. 2001, pp. 241–250 (2001)
Clark, G., Sanders, W.H.: Implementing a Stochastic Process Algebra within the Möbius Modeling Framework. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 200–215. Springer, Heidelberg (2001)
TwoTowers 5.1. http://www.sti.uniurb.it/bernardo/twotowers/
Hermanns, H., Mertsiotakis, V.: A Stochastic Process Algebra Based Modelling Tool. In: Proc. of the 11th UK Performance Engineering Workshop for Computer and Telecommunication Systems, Springer, Heidelberg (1995)
Hermanns, H., Herzog, U., Klehmet, U., Mertsiotakis, V., Siegle, M.: Compositional Performance Modelling with the TIPPtool. In: Puigjaner, R., Savino, N.N., Serra, B. (eds.) TOOLS 1998. LNCS, vol. 1469, p. 51. Springer, Heidelberg (1998)
Cleaveland, W.R., Sims, S.T.: The NCSU Concurrency Workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394–397. Springer, Heidelberg (1996)
Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)
Bohnenkamp, H., Courtney, T., Daly, D., Derisavi, S., Hermanns, H., Katoen, J.-P., Klaren, R., Lamb, V., Sanders, W.H.: On integrating the Möbius and Modest modeling tools. In: Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN’03), IEEE Computer Society Press, Los Alamitos (2003)
Garavel, H., Lang, F., Mateescu, R.: An overview of CADP 2001. Technical Report RT-254, INRIA (2001)
Clark, G.: An Extended Weak Isomorphism for Model Simplification. In: Brinksma, E., Nymeyer, A. (eds.) Proc. of 5th Process Algebra and Performance Modelling Workshop (1997)
Mertsiotakis, V.: Approximate Analysis Methods for Stochastic Process Algebras. PhD thesis, Universität Erlangen–Nürnberg, Erlangen (September 1998)
Hermanns, H., Rettelbach, M.L.: Syntax, Semantics, Equivalences and Axioms for MTIPP. In: Herzog, U., Rettelbach, M. (eds.) Proc. of 2nd Process Algebra and Performance Modelling Workshop (1994)
Bernardo, M.: Behavioural equivalences and model manipulations. In: Bernardo, M., Hillston, J., (eds.) Formal Methods for Performance Evaluation. LNCS. Springer (2007)
Hillston, J.: Fluid flow approximation of PEPA models. In: Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, Torino, Italy, Sep. 2005, pp. 33–43. IEEE Computer Society Press, Los Alamitos (2005)
Jarvis, S. (ed.): Proceedings of the Ninteenth UK Performance Engineering Workshop, University of Warwick (July 2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this chapter
Cite this chapter
Clark, A., Gilmore, S., Hillston, J., Tribastone, M. (2007). Stochastic Process Algebras. In: Bernardo, M., Hillston, J. (eds) Formal Methods for Performance Evaluation. SFM 2007. Lecture Notes in Computer Science, vol 4486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72522-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-72522-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72482-7
Online ISBN: 978-3-540-72522-0
eBook Packages: Computer ScienceComputer Science (R0)