Analysis of dynamic evolution systems by spotlight abstraction refinement

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.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Oldenburg

Year

2009

Author dc:creator

• Toben, Tobe

• [Keine Schlagwörter von Autor/in vergeben.]

Repository record source_url

http://oops.uni-oldenburg.de/821

OAI identifier oai:identifier

oai:oops.uni-oldenburg.de:821