CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishSelf-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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | Formal Analysis and Verification of Self-Healing Systems | |
| Autori: | ||
| Data di pubblicazione: | 2010 | |
| 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. | |
| Handle: | http://hdl.handle.net/11582/6648 | |
| ISBN: | 9783642120282 | |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
http://hdl.handle.net/11582/6648
Copyright © 2021