Abstract
Self-healing (SH-)systems are characterized by an automatic discovery of system failures, and techniques how to recover from these situations. In this paper, we show how to model SH-systems using algebraic graph transformation. These systems are modeled as typed graph grammars enriched with graph constraints. This allows not only for formal modeling of consistency and operational properties, but also for their analysis and verification using the tool AGG. We present sufficient static conditions for self-healing properties, deadlock-freeness and liveness of SH-systems. The overall approach is applied to a traffic light system case study, where the corresponding properties are verified.
Some of the authors are partly supported by the European Community’s Seventh Framework Programme FP7/2007-2013 under grant agreement 215483 (S-Cube) and the Italian PRIN d-ASAP project.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Brun, Y., Marzo Serugendo, G., Gacek, C., Giese, H., Kienle, H., Litoiu, M., Müller, H., Pezzè, M., Shaw, M.: Engineering self-adaptive systems through feedback loops. In: Software Engineering for Self-Adaptive Systems, pp. 48–70 (2009)
Andersson, J., Lemos, R., Malek, S., Weyns, D.: Modeling dimensions of self-adaptive software systems. In: Cheng, B.H.C., de Lemos, R., Giese, H., Inverardi, P., Magee, J. (eds.) Software Engineering for Self-Adaptive Systems. LNCS, vol. 5525, pp. 27–47. Springer, Heidelberg (2009)
Rodosek, G.D., Geihs, K., Schmeck, H., Burkhard, S.: Self-healing systems: Foundations and challenges. In: Self-Healing and Self-Adaptive Systems, Germany. Dagstuhl Seminar Proceedings, vol. 09201 (2009)
Kephart, J.O., Chess, D.M.: The vision of autonomic computing. Computer 36(1), 41–50 (2003)
White, S.R., Hanson, J.E., Whalley, I., Chess, D.M., Segal, A., Kephart, J.O.: Autonomic computing: Architectural approach and prototype. Integr. Comput.-Aided Eng. 13(2), 173–188 (2006)
Bucchiarone, A., Pelliccione, P., Vattani, C., Runge, O.: Self-repairing systems modeling and verification using AGG. In: WICSA 2009 (2009)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. EATCS Monographs in Theor. Comp. Science. Springer, Heidelberg (2006)
Ehrig, H., Engels, G., Kreowski, H.J., Rozenberg, G. (eds.): Handbook of Graph Grammars and Computing by Graph Transformation. Applications, Languages and Tools, vol. 2. World Scientific, Singapore (1999)
Ehrig, H., Ermel, C., Runge, O., Bucchiarone, A., Pelliccione, P.: Formal analysis and verication of self-healing systems: Long version. Technical report, TU Berlin (2010), http://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2010
Perry, D., Wolf, A.: Foundations for the Study of Software Architecture. SIGSOFT Softw. Eng. Notes 17(4), 40–52 (1992)
Kramer, J., Magee, J.: Self-managed systems: an architectural challenge. In: FOSE, pp. 259–268 (2007)
Floch, J., Hallsteinsen, S., Stav, E., Eliassen, F., Lund, K., Gjorven, E.: Using architecture models for runtime adaptability. IEEE Software 23(2), 62–70 (2006)
Garlan, D., Schmerl, B.: Model-based adaptation for self-healing systems. In: WOSS 2002, pp. 27–32. ACM, New York (2002)
Becker, B., Giese, H.: Modeling of correct self-adaptive systems: A graph transformation system based approach. In: Soft Computing as Transdisciplinary Science and Technology (CSTST 2008), pp. 508–516. ACM Press, New York (2008)
Bucchiarone, A.: Dynamic software architectures for global computing systems. PhD thesis, IMT Institute for Advanced Studies, Lucca, Italy (2008)
Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic invariant verification for systems with dynamic structural adaptation. In: Int. Conf. on Software Engineering (ICSE). ACM Press, New York (2006)
Baresi, L., Heckel, R., Thone, S., Varro, D.: Style-based refinement of dynamic software architectures. In: WICSA 2004. IEEE Computer Society, Los Alamitos (2004)
Hirsch, D., Inverardi, P., Montanari, U.: Modeling software architectures and styles with graph grammars and constraint solving. In: WICSA, pp. 127–144 (1999)
Métayer, D.L.: Describing software architecture styles using graph grammars. IEEE Trans. Software Eng. 24(7), 521–533 (1998)
Kastenberg, H., Rensink, A.: Model checking dynamic states in groove. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 299–305. Springer, Heidelberg (2006)
Aguirre, N., Maibaum, T.S.E.: Hierarchical temporal specifications of dynamically reconfigurable component based systems. ENTCS 108, 69–81 (2004)
Rensink, A., Schmidt, A., Varr’o, D.: Model checking graph transformations: A comparison of two approaches. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 226–241. Springer, Heidelberg (2004)
Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science, vol. 4. Springer, Heidelberg (1985)
Spanoudakis, G., Zisman, A., Kozlenkov, A.: A service discovery framework for service centric systems. In: IEEE SCC, pp. 251–259 (2005)
Canfora, G., Penta, M.D., Esposito, R., Villani, M.L.: An approach for qos-aware service composition based on genetic algorithms. In: GECCO, pp. 1069–1075 (2005)
Zeng, L., Benatallah, B., Dumas, M., Kalagnanam, J., Sheng, Q.Z.: Quality driven web services composition. In: WWW, pp. 411–421 (2003)
Baresi, L., Guinea, S., Pasquale, L.: Self-healing BPEL processes with Dynamo and the JBoss rule engine. In: ESSPE 2007, pp. 11–20. ACM, New York (2007)
Colombo, M., Nitto, E.D., Mauri, M.: Scene: A service composition execution environment supporting dynamic changes disciplined through rules. In: ICSOC, pp. 191–202 (2006)
Rukzio, E., Siorpaes, S., Falke, O., Hussmann, H.: Policy based adaptive services for mobile commerce. In: WMCS 2005. IEEE Computer Society, Los Alamitos (2005)
Inverardi, P., Pelliccione, P., Tivoli, M.: Towards an assume-guarantee theory for adaptable systems. In: SEAMS, pp. 106–115. IEEE Computer Society, Los Alamitos (2009)
Ehrig, H., Habel, A., Lambers, L.: Parallelism and Concurrency Theorems for Rules with Nested Application Conditions. In: EC-EASST (to appear, 2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ehrig, H., Ermel, C., Runge, O., Bucchiarone, A., Pelliccione, P. (2010). Formal Analysis and Verification of Self-Healing Systems. In: Rosenblum, D.S., Taentzer, G. (eds) Fundamental Approaches to Software Engineering. FASE 2010. Lecture Notes in Computer Science, vol 6013. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12029-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-12029-9_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12028-2
Online ISBN: 978-3-642-12029-9
eBook Packages: Computer ScienceComputer Science (R0)