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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
.
References
An architectural blueprint for autonomic computing. Technical report, IBM, June 2005
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
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
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)
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)
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
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)
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
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)
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)
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)
Ramirez, A.J.: Design patterns for developing dynamically adaptive systems. Master’s thesis, Michigan State University (2008)
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)
Roscoe, A.: Understanding Concurrent Systems. Springer, London (2010)
Seif, S.: Formalisation and analysis of design patterns for self-adaptive systems and their formal relationship. Master’s thesis, Techn. Universität Berlin (2015)
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
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)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)