direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Publications Prof. Hartmut Ehrig (TFS)

Formal Analysis and Verification of Self-Healing Systems
Zitatschlüssel EER+10
Autor Ehrig,H. and Ermel, C. and Runge, O. and Bucchiarone, A. and Pelliccione, P.
Buchtitel Proc. Intern. Conf. on Fundamental Aspects of Software Engineering (FASE'10)
Seiten 139–153
Jahr 2010
ISBN ISSN 0302-9743
Jahrgang 6013
Herausgeber D. Rosenblum and G. Taentzer
Verlag SPRINGER
Serie LNCS
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.
Link zur Publikation Download Bibtex Eintrag

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe