TU Berlin

Theor. Informatik / Formale SpezifikationOlga Runges Publikationen

Logo der Abteilung TFS

Inhalt des Dokuments

zur Navigation

Publications Olga Runge

Formal Analysis and Verication of Self-Healing Systems: Long Version
Zitatschlüssel EER+10b
Autor Ehrig, H. and Ermel, C. and Runge, O. and Bucchiarone, A. and Pelliccione, P.
Jahr 2010
ISBN ISSN 1436-9915
Nummer 2010/04
Notiz Available online at \urlhttp://www.eecs.tu-berlin.de/menue/forschung/forschungsberichte/2010
Institution Technische Universität Berlin
Zusammenfassung 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 formal analysis and veri cation 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. This report is the long version (including proofs of technical theorems and the complete case study) of our paper at FASE 2010.
Link zur Publikation Download Bibtex Eintrag

Navigation

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe