Parallel als Ausdruck vorh ; Zugl.: Oldenburg, Univ., Diss., 2009
Hochschulschrift
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. <dt.>
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. <engl.>
