Skip to main content
SpringerLink
Log in

Abstract Interpretation of PEPA Models

  • Chapter
  • First Online:
Semantics, Logics, and Calculi

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9560))

  • 947 Accesses

Abstract

This paper relates the fluid-flow semantics of the stochastic process algebra PEPA (Performance Evaluation Process Algebra) to the static analysis technique of abstract interpretation. The explanation in the paper is illustrated through the example of a distributed denial of service (DDoS) attack which is being launched against a server. DDoS attacks are mounted by a large population of attackers, who are coordinating and working together in attacking a specific server. The scale of the attack is crucial to its success, but the resulting large number of states in the system makes it difficult to model and analyse using the conventional discrete-state interpretation of PEPA.

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 EPUB and 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

References

  1. Yüksel, E., Nielson, H.R., Nielson, F.: Key update assistant for resource-constrained networks. In: 2012 IEEE Symposium on Computers and Communications, ISCC 2012, Cappadocia, 1–4 July 2012, pp. 75–81. IEEE (2012)

    Google Scholar 

  2. Nielson, F., Nielson, H.R., Zeng, K.: Stochastic model checking of the stochastic quality calculus. In: De Nicola, R., Hennicker, R. (eds.) Wirsing Festschrift. LNCS, vol. 8950, pp. 522–537. Springer, Heidelberg (2015)

    Google Scholar 

  3. Hillston, J.: The benefits of sometimes not being discrete. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 7–22. Springer, Heidelberg (2014)

    Google Scholar 

  4. Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, New York (1996)

    Book  Google Scholar 

  5. Yang, F.: Static Analysis of Stochastic Process Algebras. MSc dissertation (2007)

    Google Scholar 

  6. Cousot, P.: Abstract interpretation based formal methods and future challenges. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, p. 138. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Hillston, J.: Fluid flow approximation of PEPA models. In: Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, pp. 33–43. IEEE Computer Society Press, Torino, September 2005

    Google Scholar 

  8. Danos, V., Feret, J., Fontana, W., Krivine, J.: Abstract interpretation of cellular signalling networks. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 83–97. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Vigo, R., Nielson, F., Nielson, H.R.: Broadcast, denial-of-service, and secure communication. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 412–427. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. Wang, S., Nielson, F., Nielson, H.R.: A framework for hybrid systems with denial-of-service security attack. CoRR, abs/1403.6367 (2014)

    Google Scholar 

  11. Wang, S., Nielson, F., Nielson, H.R.: Denial-of-service security attack in the continuous-time world. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 149–165. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  12. Nielson, H.R., Nielson, F., Vigo, R.: A calculus for quality. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 188–204. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  13. Zeng, K., Nielson, F., Nielson, H.R.: The stochastic quality calculus. In: Kühn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 179–193. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  14. Buchholtz, M., Gilmore, S., Hillston, J., Nielson, F.: Securing statically-verified communications protocols against timing attacks. In: Bradley, J., Knottenbelt, W. (eds.) Proceedings of the First International Workshop on Practical Applications of Stochastic Modelling, pp. 61–79. England, London (2004)

    Google Scholar 

  15. Clark, A., Gilmore, S., Hillston, J., Tribastone, M.: Stochastic process algebras. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 132–179. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Bravetti, M., Gilmore, S., Guidi, C., Tribastone, M.: Replicating Web services for scalability. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 204–221. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Cappello, I., Clark, A., Gilmore, S., Latella, D., Loreti, M., Quaglia, P., Schivo, S.: Quantitative analysis of services. In: Wirsing, M., Hölzl, M. (eds.) SENSORIA. LNCS, vol. 6582, pp. 522–540. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Tribastone, M., Gilmore, S.: Automatic extraction of PEPA performance models from UML activity diagrams annotated with the MARTE profile. In: Proceedings of the 7th International Workshop on Software and Performance (WOSP2008), pp. 67–78. ACM Press, Princeton (2008)

    Google Scholar 

  20. Tribastone, M., Gilmore, S.: Automatic translation of UML sequence diagrams into PEPA models. In: 5th International Conference on the Quantitative Evaluation of Systems (QEST 2008), pp. 205–214. IEEE Computer Society Press, St Malo (2008)

    Google Scholar 

  21. Zhao, Y., Thomas, N.: Approximate solution of a PEPA model of a key distribution centre. In: Kounev, S., Gorton, I., Sachs, K. (eds.) SIPEW 2008. LNCS, vol. 5119, pp. 44–57. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Bradley, J.T., Gilmore, S., Hillston, J.: Analysing distributed Internet worm attacks using continuous state-space approximation of process algebra models. J. Comput. Syst. Sci. 74(6), 1013–1032 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  23. 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)

    Chapter  Google Scholar 

  24. Hillston, J.: Fluid flow approximation of PEPA models. In: Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), 19–22 September 2005, pp. 33–43. IEEE Computer Society, Torino (2005)

    Google Scholar 

  25. Kurtz, T.G.: Solutions of ordinary differential equations as limits of pure jump markov processes. J. Appl. Probab. 7, 49–58 (1970)

    Article  MATH  MathSciNet  Google Scholar 

  26. Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE Trans. Softw. Eng. 38(1), 205–219 (2012)

    Article  Google Scholar 

  27. Tribastone, M., Ding, J., Gilmore, S., Hillston, J.: Fluid rewards for a stochastic process algebra. IEEE Trans. Softw. Eng. 38(4), 861–874 (2012)

    Article  Google Scholar 

  28. Gilmore, S., Hillston, J., Ribaudo, M.: An efficient algorithm for aggregating PEPA models. IEEE Trans. Softw. Eng. 27(5), 449–464 (2001)

    Article  Google Scholar 

  29. Tribastone, M., Duguid, A., Gilmore, S.: The PEPA eclipse plug-in. Perform. Eval. Rev. 36(4), 28–33 (2009)

    Article  Google Scholar 

  30. Williams, C.D., Hillston, J.: Automated capacity planning for PEPA models. In: Horváth, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 209–223. Springer, Heidelberg (2014)

    Google Scholar 

  31. Poli, R., Kennedy, J., Blackwell, T.: Particle swarm optimization; an overview. Swarm Intell. 1(1), 33–57 (2007)

    Article  Google Scholar 

Download references

Acknowledgements

This work is supported by the EU project QUANTICOL, 600708. The authors thank Mirco Tribastone for useful discussions.

Author information

Authors and Affiliations

  1. Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland

    Stephen Gilmore, Jane Hillston & Natalia Zoń

Authors
  1. Stephen Gilmore
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jane Hillston
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Natalia Zoń
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jane Hillston .

Editor information

Editors and Affiliations

  1. Technical University of Denmark, Kongens Lyngby, Denmark

    Christian W. Probst

  2. Imperial College London, London, United Kingdom

    Chris Hankin

  3. Aalborg University, Aalborg, Denmark

    René Rydhof Hansen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Gilmore, S., Hillston, J., Zoń, N. (2016). Abstract Interpretation of PEPA Models. In: Probst, C., Hankin, C., Hansen, R. (eds) Semantics, Logics, and Calculi. Lecture Notes in Computer Science(), vol 9560. Springer, Cham. https://doi.org/10.1007/978-3-319-27810-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27810-0_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27809-4

  • Online ISBN: 978-3-319-27810-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation