Eingang zum Volltext in OOPS
Hinweis zum Urheberrecht
Dissertation zugänglich unter
URN: urn:nbn:de:gbv:715-oops-8760
URL: http://oops.uni-oldenburg.de/volltexte/2009/876/
Analysis of dynamic evolution systems by spotlight abstraction refinement
Toben, Tobe
pdf-Format:
Dokument 1.pdf (1.735 KB) (tobana09)
SWD-Schlagwörter:
Systemmodell , Prozess <Informatik> , Verbindungsstruktur , Analyse , Abstraktion
Institut:
Department für Informatik
Fakultät:
Fakultät II - Informatik, Wirtschafts- und Rechtswissenschaften
DDC-Sachgruppe:
Informatik
Dokumentart:
Dissertation
Hauptberichter:
Damm, Werner (Prof. Dr.)
Sprache:
Englisch
Tag der mündlichen Prüfung:
10.02.2009
Erstellungsjahr:
2009
Publikationsdatum:
07.04.2009
Kurzfassung in Deutsch:
Diese Arbeit entwickelt eine formale Analysemethode für Systemmodelle mit einer
sich verändernden Prozessanzahl und Verbindungsstruktur. Wir benutzen die
Technik der Spotlight-Abstraktion um eine endliche Darstellung des
Gesamtsystems und der zu prüfenden Eigenschaft zu erhalten. Basierend auf dem
abstract-check-refine Prinzip beschreiben wir eine Validierungsmethode für
abstrakte Gegenbeispiele, welche eine schrittweise Verfeinerung der Abstraktion
erlaubt. Diese Verfeinerungsmethode basiert auf zwei gegensätzlichen
Prinzipien, nämlich zum einen die Größe des Spotlights zu erhöhen sowie zum
anderen das Verhalten des abstrakten Prozesses einzuschränken. Wie wir auf der
Basis einer existierenden Modellierungssprache zeigen, kann diese iterative
Prozedur durch Hinzunahme von statisch berechneten Systeminvarianten weiter
verbessert werden. Wir evaluieren den Ansatz auf der Basis von Fallstudien
welche einen großen Bereich der adressierten Systemklasse abdecken.
Kurzfassung in Englisch:
This thesis develops a formal analysis technique for system models that
dynamically vary in size and topology. The approach employs the spotlight
abstraction principle to obtain a finite description of both the system and the
requirement. Following the abstract-check-refine paradigm, we devise a
validation method for abstract counterexamples by which we guide the refinement
of the abstraction. The refinement method itself alternates between two
complementary principles, namely between enlarging the size of the spotlight on
the one hand and refining the behaviour of the non-spotlight part of the
abstraction on the other hand. We demonstrate that the refinement procedure can
be further improved by integrating auxiliary system invariants, and we devise a
static analysis method to obtain such invariants for an existing modelling
language. We present a practical evaluation of our approach on a number of case
studies that cover a broad range of the addressed class of systems.