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 modelling of consistency and operational properties, but also for their formalanalysis and verication using the tool AGG. As main results, 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.

Formal Analysis and Verification of Self-Healing Systems / Ehrig, H.; Ermel, C.; Runge, O.; Bucchiarone, A.; Pelliccione:, P.. - STAMPA. - 6013:(2010), pp. 139-153. (Intervento presentato al convegno Fundamental Approaches to Software Engineering , 13th International Conference, FASE 2010 tenutosi a Paphos, Cyprus nel da 03/20/2010 a 03/28/2010).

Formal Analysis and Verification of Self-Healing Systems

A. Bucchiarone;
2010-01-01

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 modelling of consistency and operational properties, but also for their formalanalysis and verication using the tool AGG. As main results, 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.
2010
FASE
Berlin
Springer
9783642120282
Ehrig, H.; Ermel, C.; Runge, O.; Bucchiarone, A.; Pelliccione:, P.
Formal Analysis and Verification of Self-Healing Systems / Ehrig, H.; Ermel, C.; Runge, O.; Bucchiarone, A.; Pelliccione:, P.. - STAMPA. - 6013:(2010), pp. 139-153. (Intervento presentato al convegno Fundamental Approaches to Software Engineering , 13th International Conference, FASE 2010 tenutosi a Paphos, Cyprus nel da 03/20/2010 a 03/28/2010).
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/343347
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 35
  • ???jsp.display-item.citation.isi??? 19
social impact