Skip to main content

Refinement-Based Modelling and Verification of Design Patterns for Self-adaptive Systems

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10610))

Included in the following conference series:

Abstract

Design patterns are essential for designing complex systems by reusing recurring design principles. Various design patterns were proposed for self-adaptive systems, but their integration into a model-driven design process that, at the same time, provides formal guarantees is still a challenge. This is especially true for self-adaptive design patterns that are generic and abstract enough to provide general solutions that need to be refined prior to their concrete instantiations. In this paper, we present a structured and comprehensible modelling approach for design patterns in the refinement-based process calculus CSP. We formally show crucial properties of them and analyse the refinement-based relationship between their components, which generalises to entire patterns. Based on these analysis results, we are able to provide a first step towards a general, formally well-founded framework providing generic solutions for recurring problems in the management of self-adaptive systems.

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

Access this chapter

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

Notes

  1. 1.

    .

References

  1. An architectural blueprint for autonomic computing. Technical report, IBM, June 2005

    Google Scholar 

  2. Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: A conceptual framework for adaptation. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 240–254. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28872-2_17

    Chapter  Google Scholar 

  3. Cesari, L., De Nicola, R., Pugliese, R., Puviani, M., Tiezzi, F., Zambonelli, F.: Formalising adaptation patterns for autonomic ensembles. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 100–118. Springer, Cham (2014). doi:10.1007/978-3-319-07602-7_8

    Google Scholar 

  4. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)

    MATH  Google Scholar 

  5. Gardner, W.B., Gumtie, A., Carter, J.D.: Supporting selective formalism in CSP++ with process-specific storage. In: 12th International Conference on Embedded Software and Systems, ICESS 2015, pp. 1057–1065. IEEE (2015)

    Google Scholar 

  6. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_13

    Chapter  Google Scholar 

  7. Göthel, T., Klös, V., Bartels, B.: Modular design and verification of distributed adaptive real-time systems based on refinements and abstractions. EAI Endorsed Trans. Self-Adapt. Syst. 15(1), 5:1–5:12 (2015)

    Google Scholar 

  8. Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)

    Google Scholar 

  9. de la Iglesia, D.G., Weyns, D.: MAPE-K formal templates to rigorously design behaviors for self-adaptive systems. ACM Trans. Auton. Adapt. Syst. 10(3), 15:1–15:31 (2015)

    Article  Google Scholar 

  10. Khakpour, N., Jalili, S., Talcott, C., Sirjani, M., Mousavi, M.: Formal modeling of evolving self-adaptive systems. Sci. Comput. Program. 78(1), 3–26 (2012)

    Article  MATH  Google Scholar 

  11. Luckey, M., Engels, G.: High-quality specification of self-adaptive software systems. In: Proceedings of the 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2013, pp. 143–152. IEEE (2013)

    Google Scholar 

  12. Ramirez, A.J.: Design patterns for developing dynamically adaptive systems. Master’s thesis, Michigan State University (2008)

    Google Scholar 

  13. Ramirez, A.J., Cheng, B.H.C.: Design patterns for developing dynamically adaptive systems. In: Proceedings of the 2010 ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems, pp. 49–58. ACM (2010)

    Google Scholar 

  14. Roscoe, A.: Understanding Concurrent Systems. Springer, London (2010)

    Book  MATH  Google Scholar 

  15. Seif, S.: Formalisation and analysis of design patterns for self-adaptive systems and their formal relationship. Master’s thesis, Techn. Universität Berlin (2015)

    Google Scholar 

  16. Weyns, D., et al.: On patterns for decentralized control in self-adaptive systems. In: de Lemos, R., Giese, H., Müller, H.A., Shaw, M. (eds.) Software Engineering for Self-Adaptive Systems II. LNCS, vol. 7475, pp. 76–107. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35813-5_4

    Chapter  Google Scholar 

  17. Zhang, J., Cheng, B.H.C.: Model-based development of dynamically adaptive software. In: Proceedings of the 28th International Conference on Software Engineering, pp. 371–380. ACM (2006)

    Google Scholar 

  18. Zhang, J., Goldsby, H.J., Cheng, B.H.: Modular verification of dynamically adaptive systems. In: Proceedings of the 8th ACM International Conference on Aspect-Oriented Software Development, AOSD 2009, pp. 161–172. ACM (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Thomas Göthel .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Göthel, T., Jähnig, N., Seif, S. (2017). Refinement-Based Modelling and Verification of Design Patterns for Self-adaptive Systems. In: Duan, Z., Ong, L. (eds) Formal Methods and Software Engineering. ICFEM 2017. Lecture Notes in Computer Science(), vol 10610. Springer, Cham. https://doi.org/10.1007/978-3-319-68690-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68690-5_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68689-9

  • Online ISBN: 978-3-319-68690-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics