Stochastic Process Algebra: From an Algebraic Formalism to an Architectural Description Language

  • Marco Bernardo
  • Lorenzo Donatiello
  • Paolo Ciancarini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2459)


The objective of this tutorial is to describe the evolution of the field of stochastic process algebra in the past decade, through a presentation of the main achievements in the field. In particular, the tutorial stresses the current transformation of stochastic process algebra from a simple formalism to a fully fledged architectural description language for the functional verification and performance evaluation of complex computer, communication and software systems.


Model Check Semantic Model Label Transition System Architectural Style Discrete Time Markov Chain 
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.


  1. 1.
    M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, G. Franceschinis, “Modelling with Generalized Stochastic Petri Nets”, John Wiley & Sons, 1995Google Scholar
  2. 2.
    A. Aldini, M. Bernardo, R. Gorrieri, “An Algebraic Model for Evaluating the Performance of an ATM Switch with Explicit Rate Marking”, in Proc. of the 7th Int. Workshop on Process Algebra and Performance Modelling (PAPM 1999), Prensas Universitarias de Zaragoza, pp. 119–138, Zaragoza (Spain), 1999Google Scholar
  3. 3.
    A. Aldini, M. Bernardo, R. Gorrieri, M. Roccetti, “Comparing the QoS of Internet Audio Mechanisms via Formal Methods”, in ACM Trans. on Modeling and Computer Simulation 11:1–42, 2001CrossRefGoogle Scholar
  4. 4.
    R. Allen, D. Garlan, “A Formal Basis for Architectural Connection”, in ACM Trans. on Software Engineering and Methodology 6:213–249, 1997CrossRefGoogle Scholar
  5. 5.
    J.C.M. Baeten, W.P. Weijland, “Process Algebra”, Cambridge University Press, 1990Google Scholar
  6. 6.
    C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, “On the Logical Characterisation of Performability Properties”, in Proc. of the 27th Int. Coll. on Automata, Languages and Programming (ICALP 2000), LNCS 1853:780–792, Geneve (Switzerland), 2000Google Scholar
  7. 7.
    C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, “Model Checking Continuous-Time Markov Chains by Transient Analysis”, in Proc. of the 12th Int. Conf. on Computer Aided Verification (CAV 2000), LNCS 1855:358–372, Chicago (IL), 2000Google Scholar
  8. 8.
    C. Baier, J.-P. Katoen, H. Hermanns, “Approximate Symbolic Model Checking of Continuous Time Markov Chains”, in Proc. of the 10th Int. Conf. on Concurrency Theory (CONCUR 1999), LNCS 1664:146–162, Eindhoven (The Netherlands), 1999Google Scholar
  9. 9.
    S. Balsamo, M. Bernardo, M. Simeoni, “Combining Stochastic Process Algebras and Queueing Networks for Software Architecture Analysis”, to appear in Proc. of the 3rd Int. Workshop on Software and Performance (WOSP 2002), Rome (Italy), 2002Google Scholar
  10. 10.
    M. Bernardo, “Theory and Application of Extended Markovian Process Algebra”, Ph.D. Thesis, University of Bologna (Italy), 1999Google Scholar
  11. 11.
    M. Bernardo, “A Simulation Analysis of Dynamic Server Selection Algorithms for Replicated Web Services”, in Proc. of the 9th Int. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2001), IEEE-CS Press, pp. 371–378, Cincinnati (OH), 2001Google Scholar
  12. 12.
    M. Bernardo, M. Bravetti, “Reward Based Congruences: Can We Aggregate More?”, in Proc. of the 1st Joint Int. Workshop on Process Algebra and Performance Modelling and Probabilistic Methods in Verification (PAPM/PROBMIV 2001), LNCS 2165:136–151, Aachen (Germany), 2001Google Scholar
  13. 13.
    M. Bernardo, M. Bravetti, “Performance Measure Sensitive Congruences for Markovian Process Algebras”, to appear in Theoretical Computer Science, 2002Google Scholar
  14. 14.
    M. Bernardo, N. Busi, M. Ribaudo, “Integrating TwoTowers and GreatSPN through a Compact Net Semantics”, to appear in Performance Evaluation, 2002Google Scholar
  15. 15.
    M. Bernardo, P. Ciancarini, L. Donatiello, “ÆMPA: A Process Algebraic Description Language for the Performance Analysis of Software Architectures”, in Proc. of the 2nd Int. Workshop on Software and Performance (WOSP 2000), ACM Press, pp. 1–11, Ottawa (Canada), 2000Google Scholar
  16. 16.
    M. Bernardo, P. Ciancarini, L. Donatiello, “Architecting Software Systems with Process Algebras”, Tech. Rep. UBLCS-2001-07, University of Bologna (Italy), 2001Google Scholar
  17. 17.
    M. Bernardo, W.R. Cleaveland, “A Theory of Testing for Markovian Processes”, in Proc. of the 11th Int. Conf. on Concurrency Theory (CONCUR 2000), LNCS 1877:305-319, State College (PA), 2000Google Scholar
  18. 18.
    M. Bernardo, W.R. Cleaveland, W.S. Stewart, “TwoTowers 1.0 User Manual”,, 2001
  19. 19.
    M. Bernardo, F. Franzè, “Architectural Types Revisited: Extensible And/Or Connections”, in Proc. of the 5th Int. Conf. on Fundamental Approaches to Software Engineering (FASE 2002), LNCS 2306:113–128, Grenoble (France), 2002Google Scholar
  20. 20.
    M. Bernardo, F. Franzè, “Exogenous and Endogenous Extensions of Architectural Types”, in Proc. of the 5th Int. Conf. on Coordination Models and Languages (COORDINATION 2002), LNCS 2315:40–55, York (UK), 2002Google Scholar
  21. 21.
    M. Bernardo, R. Gorrieri, M. Roccetti, “Formal Performance Modelling and Evaluation of an Adaptive Mechanism for Packetised Audio over the Internet”, in Formal Aspects of Computing 10:313–337, 1999CrossRefGoogle Scholar
  22. 22.
    H. Bohnenkamp, “Compositional Solution of Stochastic Process Algebra Models”, Ph.D. Thesis, RWTH Aachen (Germany), 2001Google Scholar
  23. 23.
    H. Bowman, J.W. Bryans, J. Derrick, “Analysis of a Multimedia Stream using Stochastic Process Algebra”, in Proc. of the 6th Int. Workshop on Process Algebra and Performance Modelling (PAPM 1998), pp. 51–69, Nice (France), 1998Google Scholar
  24. 24.
    J.T. Bradley, “Towards Reliable Modelling with Stochastic Process Algebras”, Ph.D. Thesis, University of Bristol (UK), 1999Google Scholar
  25. 25.
    M. Bravetti, “Specification and Analysis of Stochastic Real-Time Systems”, Ph.D. Thesis, University of Bologna (Italy), 2002Google Scholar
  26. 26.
    M. Bravetti, M. Bernardo, “Compositional Asymmetric Cooperations for Process Algebras with Probabilities, Priorities, and Time”, in Proc. of the 1st Int. Workshop on Models for Time Critical Systems (MTCS 2000), Electronic Notes in Theoretical Computer Science 39(3), State College (PA), 2000Google Scholar
  27. 27.
    P. Buchholz, “Markovian Process Algebra: Composition and Equivalence”, in Proc. of the 2nd Int. Workshop on Process Algebra and Performance Modelling (PAPM 1994), pp. 11–30, Erlangen (Germany), 1994Google Scholar
  28. 28.
    W.R. Cleaveland, J. Parrow, B. Steffen, “The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems”, in ACM Trans. on Programming Languages and Systems 15:36–72, 1993CrossRefGoogle Scholar
  29. 29.
    G. Clark, “Techniques for the Construction and Analysis of Algebraic Performance Models”, Ph.D. Thesis, University of Edinburgh (UK), 2000Google Scholar
  30. 30.
    E.M. Clarke, O. Grumberg, D.A. Peled, “Model Checking”, MIT Press, 1999Google Scholar
  31. 31.
    P. D’Argenio, “Algebras and Automata for Timed and Stochastic Systems”, Ph.D. Thesis, University of Twente (The Netherlands), 1999Google Scholar
  32. 32.
    R. De Nicola, M.C.B. Hennessy, “Testing Equivalences for Processes”, in Theoretical Computer Science 34:83–133, 1983CrossRefGoogle Scholar
  33. 33.
    D. Ferrari, “Considerations on the Insularity of Performance Evaluation”, in IEEE Trans. on Software Engineering 12:678–683, 1986Google Scholar
  34. 34.
    S. Gilmore, “The PEPA Workbench User Manual”,, 2001
  35. 35.
    S. Gilmore, J. Hillston, D.R.W. Holton, M. Rettelbach, “Specifications in Stochastic Process Algebra for a Robot Control Problem”, in Journal of Production Research 34:1065–1080, 1996zbMATHCrossRefGoogle Scholar
  36. 36.
    R.J. van Glabbeek, S.A. Smolka, B. Steffen, “Reactive, Generative and Stratified Models of Probabilistic Processes”, in Information and Computation 121:59–80, 1995zbMATHCrossRefMathSciNetGoogle Scholar
  37. 37.
    R.J. van Glabbeek, F.W. Vaandrager, “Petri Net Models for Algebraic Theories of Concurrency”, in Proc. of the Conf. on Parallel Architectures and Languages Europe (PARLE 1987), LNCS 259:224–242, Eindhoven (The Netherlands), 1987Google Scholar
  38. 38.
    N. Götz, “Stochastische Prozeßalgebren-Integration von funktionalem Entwurf und Leistungsbewertung Verteilter Systeme”, Ph.D. Thesis, University of Erlangen (Germany), 1994Google Scholar
  39. 39.
    P.G. Harrison, J. Hillston, “Exploiting Quasi-Reversible Structures in Markovian Process Algebra Models”, in Computer Journal 38:510–520, 1995CrossRefGoogle Scholar
  40. 40.
    H. Hermanns, “Interactive Markov Chains”, Ph.D. Thesis, University of Erlangen (Germany), 1998Google Scholar
  41. 41.
    H. Hermanns, U. Herzog, J. Hillston, V. Mertsiotakis, M. Rettelbach, “Stochastic Process Algebras: Integrating Qualitative and Quantitative Modelling”, Tech. Rep. 11/94, University of Erlangen (Germany), 1994Google Scholar
  42. 42.
    H. Hermanns, U. Herzog, V. Mertsiotakis, “Stochastic Process Algebras as a Tool for Performance and Dependability Modelling”, in Proc. of the 1st IEEE Int. Computer Performance and Dependability Symp. (IPDS 1995), IEEE-CS Press, pp. 102–111, Erlangen (Germany), 1995Google Scholar
  43. 43.
    H. Hermanns, J.-P. Katoen, “Automated Compositional Markov Chain Generation for a Plain-Old Telephone System”, in Science of Computer Programming 36:97–127, 2000zbMATHCrossRefGoogle Scholar
  44. 44.
    H. Hermanns, J. Meyer-Kayser, M. Siegle, “Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains”, in Proc. of the 3rd Int. Workshop on the Numerical Solution of Markov Chains (NSMC 1999), Zaragoza (Spain), 1999Google Scholar
  45. 45.
    H. Hermanns, M. Rettelbach, “Syntax, Semantics, Equivalences, and Axioms for MTIPP”, in Proc. of the 2nd Int. Workshop on Process Algebra and Performance Modelling (PAPM 1994), pp. 71–87, Erlangen (Germany), 1994Google Scholar
  46. 46.
    U. Herzog, “Formal Description, Time and Performance Analysis-A Framework”, in Entwurf und Betrieb verteilter Systeme, Informatik Fachberichte 264, Springer, 1990Google Scholar
  47. 47.
    U. Herzog, “EXL: Syntax, Semantics and Examples”, Tech. Rep. 16/90, University of Erlangen (Germany), 1990Google Scholar
  48. 48.
    J. Hillston, “A Compositional Approach to Performance Modelling”, Cambridge University Press, 1996Google Scholar
  49. 49.
    J. Hillston, N. Thomas, “Product Form Solution for a Class of PEPA Models”, in Performance Evaluation 35:171–192, 1999zbMATHCrossRefGoogle Scholar
  50. 50.
    C.A.R. Hoare, “Communicating Sequential Processes”, Prentice Hall, 1985Google Scholar
  51. 51.
    D.R.W. Holton, “A PEPA Specification of an Industrial Production Cell”, in Computer Journal 38:542–551, 1995CrossRefGoogle Scholar
  52. 52.
    R.A. Howard, “Dynamic Probabilistic Systems”, John Wiley & Sons, 1971Google Scholar
  53. 53.
    K. Kanani, “A Unified Framework for Systematic Quantitative and Qualitative Analysis of Communicating Systems”, Ph.D. Thesis, Imperial College (UK), 1998Google Scholar
  54. 54.
    J.-P. Katoen “Quantitative and Qualitative Extensions of Event Structures”, Ph.D. Thesis, University of Twente (The Netherlands), 1996Google Scholar
  55. 55.
    U. Klehmet, V. Mertsiotakis, “TIPPtool-User’s Guide”,, 1998
  56. 56.
    L. Kleinrock, “Queueing Systems”, John Wiley & Sons, 1975Google Scholar
  57. 57.
    K.G. Larsen, A. Skou, “Bisimulation through Probabilistic Testing”, in Information and Computation 94:1–28, 1991zbMATHCrossRefMathSciNetGoogle Scholar
  58. 58.
    S.S. Lavenberg editor, “Computer Performance Modeling Handbook”, Academic ress, 1983Google Scholar
  59. 59.
    V. Mertsiotakis, “Approximate Analysis Methods for Stochastic Process Algebras”, Ph.D. Thesis, University of Erlangen (Germany), 1998Google Scholar
  60. 60.
    R. Milner, “Communication and Concurrency”, Prentice Hall, 1989Google Scholar
  61. 61.
    D.E. Perry, A.L. Wolf, “Foundations for the Study of Software Architecture”, in ACM SIGSOFT Software Engineering Notes 17:40–52, 1992CrossRefGoogle Scholar
  62. 62.
    M. Rettelbach, “Stochastische Prozeßalgebren mit zeitlosen Aktivitäten und probabilistischen Verzweigungen”, Ph.D. Thesis, University of Erlangen (Germany), 1996Google Scholar
  63. 63.
    M. Ribaudo, “On the Relationship between Stochastic Process Algebras and Stochastic Petri Nets”, Ph.D. Thesis, University of Torino (Italy), 1995Google Scholar
  64. 64.
    P. Schweitzer, “Aggregation Methods for Large Markov Chains”, in Mathematical Computer Performance and Reliability, North Holland, pp. 275–286, 1984Google Scholar
  65. 65.
    M. Sereno, “Towards a Product Form Solution for Stochastic Process Algebras”, in Computer Journal 38:622–632, 1995CrossRefGoogle Scholar
  66. 66.
    M. Shaw, D. Garlan, “Software Architecture: Perspectives on an Emerging Discipline”, Prentice Hall, 1996Google Scholar
  67. 67.
    M. Siegle, “Beschreibung und Analyse von Markovmodellen mit grossem Zustandsraum”, Ph.D. Thesis, University of Erlangen (Germany), 1995Google Scholar
  68. 68.
    C.U. Smith, “Performance Engineering of Software Systems”, Addison-Wesley, 1990Google Scholar
  69. 69.
    W.J. Stewart, “Introduction to the Numerical Solution of Markov Chains”, Princeton University Press, 1994Google Scholar
  70. 70.
    B. Strulo, “Process Algebra for Discrete Event Simulation”, Ph.D. Thesis, Imperial College (UK), 1994Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Marco Bernardo
    • 1
  • Lorenzo Donatiello
    • 2
  • Paolo Ciancarini
    • 2
  1. 1.Centro per l’Appl. delle Sc. e Tecn. dell’Inf.Università di UrbinoUrbinoItaly
  2. 2.Dipartimento di Scienze dell’InformazioneUniversità di BolognaBolognaItaly

Personalised recommendations