Specifying Performance Measures for PEPA

  • Graham Clark
  • Stephen Gilmore
  • Jane Hillston
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1601)


Stochastic process algebras such as PEPA provide ample support for the component-based construction of models. Tools compute the numerical solution of these models; however, the stochastic process algebra methodology lacks support for the specification and calculation of complex performance measures. This paper addresses that problem by presenting a performance specification language which supports high level reasoning about PEPA models, allowing the description of equilibrium (steady-state) measures. The meaning of the specification language can be made formal by examining its foundations in a stochastic modal logic. A case-study is presented to illustrate the approach.


Model Check Modal Logic Continuous Time Markov Chain Reward Structure Throughput Measure 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.Google Scholar
  2. [2]
    S. Gilmore and J. Hillston. The PEPA Workbench: A Tool to Support a Process Algebra-based Approach to Performance Modelling. In G. Haring and G. Kotsis, editors, Proceedings of 7th Conf. on Mod. Techniques and Tools for Computer Perf. Eval., volume 794 of LNCS, pages 353–368, 1994.Google Scholar
  3. [3]
    N. Götz, U. Herzog, and M. Rettelbach. Multiprocessor and Distributed System Design: The Integration of Functional Specification and Performance Analysis using Stochastic Process Algebras. In Performance’93, 1993.Google Scholar
  4. [4]
    M. Bernardo, L. Donatiello, and R. Gorrieri. Integrating Performance and Functional Analysis of Concurrent Systems with EMPA. Technical Report UBLCS-95-14, University of Bologna, 1995.Google Scholar
  5. [5]
    R. A. Howard. Dynamic Probabilistic Systems, volume II: Semi-Markov and Decision Processes, chapter 13, pages 851–915. John Wiley & Sons, New York, 1971.Google Scholar
  6. [6]
    H. Bowman. Analysis of a Multimedia Stream using Stochastic Process Algebra. In Priami [23], pages 51–69.Google Scholar
  7. [7]
    G. Clark. Formalising the Specification of Rewards with PEPA. In Proceedings of the Fourth Process Algebras and Performance Modelling Workshop, pages 139–160, July 1996.Google Scholar
  8. [8]
    G. Clark and J. Hillston. Towards Automatic Derivation of Performance Measures from PEPA Models. Proceedings of UKPEW, September 1996.Google Scholar
  9. [9]
    S. Gilmore and J. Hillston. Feature Interaction in PEPA. In Priami [23], pages 17–26.Google Scholar
  10. [10]
    S. Gilmore, J. Hillston, and L. Recalde. Elementary structural analysis for PEPA. Technical Report ECS-LFCS-97-377, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh, 1997.Google Scholar
  11. [11]
    K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, September 1991.MathSciNetCrossRefzbMATHGoogle Scholar
  12. [12]
    M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science, pages 111–122, Warsaw, Poland, 29 June–2 July 1997. IEEE Computer Society Press.Google Scholar
  13. [13]
    D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.MathSciNetCrossRefzbMATHGoogle Scholar
  14. [14]
    H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.CrossRefzbMATHGoogle Scholar
  15. [15]
    V. Hartonas-Garmhausen. Probabilistic Symbolic Model Checking with Engineering Models and Applications. PhD thesis, Carnegie Mellon University, 1998.Google Scholar
  16. [16]
    S. Campos, E. Clarke, and M. Minea. The Verus tool: A quantitative approach to the formal verification of real-time systems. Lecture Notes in Computer Science, 1254, 1997.Google Scholar
  17. [17]
    M. Bernardo. An Algebra-Based Method to Associate Rewards with EMPA Terms. In to appear in 24th Int. Colloquium on Automata, Languages and Programming, July 1997.Google Scholar
  18. [18]
    M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, January 1985.CrossRefzbMATHGoogle Scholar
  19. [19]
    L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In LICS: IEEE Symposium on Logic in Computer Science, 1998.Google Scholar
  20. [20]
    A. Harter and A. Hopper. A distributed location system for the active office. IEEE Network Magazine, 8(1):62–70, 1994.CrossRefGoogle Scholar
  21. [21]
    Y-B. Lin and P. Lin. Performance modeling of location tracking systems. Mobile Computing and Communications Review, 2(3):24–27, 1998.CrossRefGoogle Scholar
  22. [22]
    I. Mitrani. Probabilistic Modelling. Cambridge University Press, 1998.Google Scholar
  23. [23]
    C. Priami, editor. Proceedings of the Sixth International Workshop on Process Algebras and Performance Modelling, Nice, France, September 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Graham Clark
    • 1
  • Stephen Gilmore
    • 1
  • Jane Hillston
    • 1
  1. 1.Laboratory for Foundations of Computer ScienceThe University of EdinburghEdinburghScotland

Personalised recommendations