Skip to main content
SpringerLink
Log in

Formal Methods for Performance Evaluation

  • Chapter
  • First Online:
Lectures on Formal Methods and PerformanceAnalysis (EEF School 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2090))

Included in the following conference series:

Abstract

The main goal of this contribution is to advocate the increased use of formal methods (FM) in the field of performance evaluation (PE). Moreover, we try to reduce the mutual reservations between both areas, formal specification techniques and performance evaluation since both can profit from such an integration: FMs may find their way into a new and very attractive area of applications and some fundamental problems of PE may be overcome.

The first part summarizes the evolution of PE, its methodology and the basic concepts of performance modeling and analysis, elaborated in specific contributions of this book.

Classical modeling and analysis techniques have a high standard and have been quite successful. However, there are important problem classes still open, and there are some fundamental deficiencies: Task interdependencies and synchronization, interfacing in modeling hierarchies, methods and tools for automating the performance engineering process are typical examples.

We therefore advocate the integration of FMs and PE and survey three advanced approaches, again, treated in detail in specific contributions: Stochastic Petri-Nets, Stochastic Activity Networks and Stochastic Process Algebras.

We try to summarize our own experience with these techniques and conclude with a list of challenging topics and current research directions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Ajmone Marsan, G. Balbo, and G. Conte. Performance Models of Multiprocessor Systems. MIT Press, 1986.

    Google Scholar 

  2. A. Aldini, M. Bernardo, and R. Gorrieri. An Algebraic Model for Evaluating the Performance of an ATM-Switch with Explicit Rate Marking. In Proceedings of the PAPM-Workshop, 1999.

    Google Scholar 

  3. G. Balbo. Introduction to Stochastic Petri Nets. This volume.

    Google Scholar 

  4. T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN System, 14, 1987.

    Google Scholar 

  5. M. Bernardo, W.R. Cleaveland, S.T. Sims, and W.J. Stewart. TwoTowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems. In FORTE/PSTV, 1998.

    Google Scholar 

  6. G. Bolch, S. Greiner, H. de Meer, and K.S. Trivedi. Queuing Networks and Markov Chains. John Wiley&Sons, 1998.

    Google Scholar 

  7. E. Brinksma and H. Hermanns. Process Algebra and Markov Chains. This volume.

    Google Scholar 

  8. F. Bause and P. Kritzinger. Stochastic Petri Nets. Vieweg, Braunschweig, 1996.

    Google Scholar 

  9. E. Brinksma, J.P. Katoen, D. Latella, and R. Langerak. Partial-order models for quantitative extensions of LOTOS. Computer Networks and ISDN Systems, 30(9/10):925–950, 1998.

    Article  Google Scholar 

  10. P. Buchholz. Markovian Process Algebra: Composition and Equivalence. In U. Herzog and M. Rettelbach, editors, Proc. of the 2nd Workshop on Process Algebras and Performance Modelling, pages 11–30, Regensberg/Erlangen, July 1994. Arbeitsberichte des IMMD, Universität Erlangen-Nürnberg.

    Google Scholar 

  11. J.P. Buzen. Queuing network models of multiprogramming. PhD thesis, Div. Eng. and Applied Physics, Harvad Univ., Cambridge, Mass., May 1971.

    Google Scholar 

  12. C. Cassandras. Discrete Event Systems: Modeling and Performance Analysis. Irwin Inc. and Aksen Associates, Inc., 1993.

    Google Scholar 

  13. G. Ciardo. Distributed and Structured Analysis Approaches to Study Large and Complex Systems. This volume, 2001.

    Google Scholar 

  14. L. Cohen. The Single Server Queue. North Holland, Amsterdam, 1969. revised 1982.

    MATH  Google Scholar 

  15. P.R. D’Argenio. Algebras and Automata for Timed and Stochastic Systems. IPA Dissertation Series 1999-10, CTIT Phd-Thesis Series 99-25, University of Twente, November 1999.

    Google Scholar 

  16. Erlang. The Application of the Theory of Probabilities in Telephone Administration. Scandinavian H.C.Örsted Congress, Copenhagen, 1920.

    Google Scholar 

  17. D. Ferrari. Considerations on the Insularity of Performance Evaluation. IEEE Transactions on Software Engineering, SE-12(6):678–683, June 1986.

    Google Scholar 

  18. H.J. Fromm, U. Hercksen, U. Herzog, K.-H. John, R. Klar, and W. Kleinöder. Experience with performance meassurement and modelling of a processor array. IEEE Trans. on Computers, C-32(1):15–31, January 1983.

    Article  Google Scholar 

  19. F. Fischer, T. Hopfner, T. Kolloch, A. Muth, S. Petters, G. Färber, M. Dörfel, W. Dulz, R. Hofmann, A. Mitschele-Thiel, R. Münzenberger, F. Slomka, and U. Herzog. Rapid Prototyping von Realzeitsystemen. it+ti, 42(2):45–53, 2000.

    Article  Google Scholar 

  20. D. Ferrari, G. Serazzi, and A. Zeigner. Measurement and Tuning of Computer Systems. Prentice Hall, Inc., Englewood Cliffs, 1983.

    Google Scholar 

  21. R. German. Non-Markovian Analysis. This volume.

    Google Scholar 

  22. D. Gross and C.M. Harris. Fundamentals of Queuing Theory. John Wiley&Sons, Second Edition, 1985.

    Google Scholar 

  23. N. Götz, U. Herzog, and M. Rettelbach. TIPP-Einführung in die Leistungsbewertung von verteilten Systemen mit Hilfe von Prozeßalgebren. In Verteilte Systeme-Grundlagen und zukünftige Entwicklungen aus der Sicht des Sonderforschungsbereichs 182 “Multiprozessor-und Netzwerkkonfigurationen”, pages 509–531. BIWissenschaftsverlag, 1993.

    Google Scholar 

  24. S. Gilmore. The PEPA workbench: A tool to support a process algebra-based approach to performance modeling. In G. Kotsis G. Haring, editor, 7th Internat. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, Wien, 1994.

    Google Scholar 

  25. R. Gorrieri. Stochastic Process Algebras; Past and Future. In J. Hillston and M. Silva, editors, Proceedings of the PAPM’99-workshop, pages 1–2, Prensas Universitarias de Zaragoza, 1999. Invited Talk at the Multi-Workshop on Formal Methods in Performance Evaluation and Applications.

    Google Scholar 

  26. B. Haverkort. Markovian Models for Performance and Dependability Evaluation. This volume.

    Google Scholar 

  27. U. Herzog. Modellierung des Ablaufgeschehens in Networks-Modelling of Network Dynamics. In Lectures and Tutorials, Information und Kommunikation, number 8, pages 175–208. Oldenbourg, Munich, 1979.

    Google Scholar 

  28. U. Herzog. A Concept for Graph-Based Stochastic Process Algebras, Generally Distributed Activity Times and Hierarchical Modelling. Technical report IMMD VII 4/96, Universität Erlangen-Nürnberg, Martensstr. 3, 91058 Erlangen, May 1996.

    Google Scholar 

  29. H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis, and M. Siegle. Compositional performance modelling with the TIPPtool. Performance Evaluation, 39(1-4):5–35, January 2000.

    Article  MATH  Google Scholar 

  30. H. Hermanns, U. Herzog, and J.-P. Katoen. Process Algebra for Performance Evaluation. Journal of Theoretical Computer Science, Elsevier, to appear 2001.

    Google Scholar 

  31. H. Hermanns, U. Herzog, and V. Mertsiotakis. Stochastic Process Algebras-between LOTOS and Markov Chains. Computer Networks and ISDN Systems, 1998.

    Google Scholar 

  32. J. Hillston. A Compositional Approach to Performance Modelling. PhD thesis, University of Edinburgh, 1994.

    Google Scholar 

  33. J. Hillston. Exploiting Structure in Solution: Decomposing Compositional Models. This volume.

    Google Scholar 

  34. H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. Towards model checking stochastic process algebra. In W. Grieskamp, T. Santen, and B. Stoddart, editors, 2nd Int. Conference on Integrated Formal Methods, pages 420–439, Dagstuhl, November 2000. Springer, LNCS 1945.

    Chapter  Google Scholar 

  35. F.S. Hillier and G.J. Liebermann. Introduction to Operations Research. Holden Day Inc., San Francisco, 1967.

    MATH  Google Scholar 

  36. G. Haring, C. Lindemann, and M. Reiser. Performance Evaluation: Origin and Directions. Number 1769 in LNCS State-of-the-Art Survey. Springer, 2000.

    Book  Google Scholar 

  37. J. Hillston and V. Mertsiotakis. A Simple Time Scale Decomposition Technique for Stochastic Process Algebras. The Computer Journal, 38(7):566–577, December 1995. Special issue: Proc. of the 3rd Workshop on Process Algebras and Performance Modelling.

    Article  Google Scholar 

  38. H. Hermanns, V. Mertsiotakis, and M. Rettelbach. A Construction and Analysis Tool Based on the Stochastic Process Algebra TIPP. In Proc. of 2nd Int.Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 427–430. Springer, LNCS 1055, 1996.

    Google Scholar 

  39. H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains. In B. Plateau, W.J. Stewart, and M. Silva, editors, 3rd Int. Workshop on the Numerical Solution of Markov Chains, pages 188–207. Prensas Universitarias de Zaragoza, 1999.

    Google Scholar 

  40. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ, 1985.

    MATH  Google Scholar 

  41. U. Herzog and J. Rolia. Performance Validation Tools for Software/Hardware Systems. Performance Evaluation, 40, to appear in 2001.

    Google Scholar 

  42. International Teletraffic Congress, since 1955. Conference and proceedings every three years.

    Google Scholar 

  43. Raj Jain. The Art of Computer Systems Performance Analysis. J. Wiley, New York, 1991. I: Overview, II: Measurement, III: Probability, IV:Experimental Design, V: Simulation, VI: Queuing Models.

    Google Scholar 

  44. J.-P. Katoen and P.R. D’Argenio. General Distributions in Process Algebra. This volume.

    Google Scholar 

  45. R. Klar, P. Dauphin, F. Hartleb, R. Hofmann, B. Mohr, A. Quick, and M. Siegle. Messung und Modellierung paralleler und verteilter Rechensystem. Teubner, 1995.

    Google Scholar 

  46. L. Kleinrock. Queueing Systems, volume 1: Theory. John Wiley & Sons, 1975.

    Google Scholar 

  47. W. Kleinöder. Stochastische Bewertung von Aufgabenstrukturen für Hierarchische Mehrrechnersysteme. IMMD, University of Erlangen, August 1982. Dissertation am Lehrstuhl 7 des IMMD.

    Google Scholar 

  48. H. Kobayashi. Modeling and Analysis-An Introduction to System Performance Evaluation Methodology. Addison-Wesley, 1978.

    Google Scholar 

  49. F. Lemmen. Spezifikationsgesteuertes Monitoring zur Integration der Leistungsbewertung in den formalen Entwurf von Kommunikationssystemen. IM M D,University of Erlangen, 2000. Dissertation am Lehrstuhl 7 des IMMD.

    Google Scholar 

  50. K. Marzbani. Hierarchische Beschreibung und Analyse von Kommunikationssystemen mittels graphbasierter Prozessalgebren. Diplomarbeit, IMMD7, Universität Erlangen-Nürnberg, März 1997.

    Google Scholar 

  51. R. Gorrieri M. Bernardo, L. Donatiello. MPA, a Stochastic Process Algebra. Technical report, University of Bologna, 1994. Techn. Report to 94-10.

    Google Scholar 

  52. R. Milner. Communication and Concurrency. Prentice Hall, London, 1989.

    MATH  Google Scholar 

  53. M.K. Molloy. On the integration of delay and throughput measures in distributed processing models. PhD thesis, University of California, Los Angeles, 1981.

    Google Scholar 

  54. M.K. Molloy. Fundamentals of Performance Modeling. Macmillan-Colliev Macmillan, 1989.

    Google Scholar 

  55. V. Mertsiotakis and M. Silva. Throughput Approximation of Decision Free Processes Using Decomposition. In Proc. of the 7th Int. Workshop on Petri Nets and Performance Models, pages 174–182, St. Malo, June 1997. IEEE CS-Press.

    Google Scholar 

  56. C.A. Petri. Kommunikation mit Automaten, 1962. Dissertation an der Universität Bonn, Schriften des Instituts für Instrumentelle Mathematik Nr. 3.

    Google Scholar 

  57. C. Priami. Stochastic p-calculus with general distributions. In Proc. of the 4th Workshop on Process Algebras and Performance Modelling, pages 41–57, Torino, July 1996. Dpto. di Informatica, Universita di Torino. To appear.

    Google Scholar 

  58. J.A. Rolia and K.C. Sevcik. The Methods of Layers. IEEE Transactions on Software Engineering, 21(8):689–700, August 1995.

    Article  Google Scholar 

  59. T.L. Saaty. Elements of Queuing Theory. With Applications. McGraw-Hill, 1961.

    Google Scholar 

  60. W. Sanders. UltraSAN User’s Manual, Version 3.0. University of Illinois, Urbana-Champaign, 1995.

    Google Scholar 

  61. W. Sanders and J.F. Meyer. Stochastic Activity Networks: Formal Definitions and Concepts. This volume.

    Google Scholar 

  62. A.L. Scherr. An Analysis of Time-Shared Computer Systems. Number 36 in Research Monograph. MIT Press, 1967.

    Google Scholar 

  63. F. Slomka, M. Dörfel, R. Münzenberger, and R. Hofmann. Hardware/Software Codesign and Rapid Prototyping of Embedded Systems. IEEE Design and Test of Computers, pages 28–38, 2000.

    Google Scholar 

  64. W.J. Stewart. Introduction to the numerical solution of Markov chains. Princeton University Press, 1994.

    Google Scholar 

  65. W.J. Stewart. Numerical Analysis Methods. In G. Haring, Ch. Lindemann, and M. Reiser, editors, Performance Evaluation: Origins and Directions, LNCS 1769, pages 355–376. Springer, Berlin, Heidelberg, 2000.

    Chapter  Google Scholar 

  66. R.v. Stieglitz. Messung und Bewertung des dynamischen Verhaltens eines Kommunikations-Prototypen für Breitband-ISDN (BERKOM). Dimplomarbeit, IMMD7, Universität Erlangen-Nürnberg, 1990.

    Google Scholar 

  67. R. Syski. Introduction to Congestion Theory in Telephone Systems. Oliver and Boyd, reprinted 1985.

    Google Scholar 

  68. P. Tran-Gia. Analytische Leistungsbewertung verteilter Systeme. Springer, 1996. in German.

    Google Scholar 

  69. Kishor S. Trivedi. Probability and Statistics with Reliability, Queuing, and Computer Science Applications. Prentice-Hall, 1982.

    Google Scholar 

  70. I. Weigel. Modelle für Entwurf und Bewertung eines dynamischen Lastverbunds lose gekoppelter Rechensysteme. IMMD, Martensstraße 3, 91058 Erlangen, März 1994. Dissertation am Lehrstuhl für Rechnerarchitektur und-Verkehrstheorie, Universität Erlangen-Nürnberg.

    Google Scholar 

  71. P. Wimmer. Lastcharakterisierung in der automatisierten Fertigung am Beispiel der Leiterplattenbestückung. Diplomarbeit, IMMD7, Universität Erlangen-Nürnberg, Januar 1991.

    Google Scholar 

  72. C.M. Woodside, J.E. Neilson, D.C. Petriu, and S. Majumdar. The Stochastic Rendezvous Network Model for Performance of Synchronous Client-Server-like Distributed Software. IEEE Transactions on Computers, 44(1):20–34, January 1995.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik 7, Universität Erlangen-Nürnberg, Rechnernetze und Kommunikationssysteme, Martensstr. 3, D, 91058, Erlangen, Germany

    Ulrich Herzog

Authors
  1. Ulrich Herzog
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Computer Science, Formal Methods and Tools Group, University of Twente, 217, 7500, AE, Enschede, The Netherlands

    Ed Brinksma , Holger Hermanns  & Joost-Pieter Katoen ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Herzog, U. (2001). Formal Methods for Performance Evaluation. In: Brinksma, E., Hermanns, H., Katoen, JP. (eds) Lectures on Formal Methods and PerformanceAnalysis. EEF School 2000. Lecture Notes in Computer Science, vol 2090. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44667-2_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-44667-2_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42479-6

  • Online ISBN: 978-3-540-44667-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation