TY  - THES
A3  - Wehrheim, Heike
A3  - Kleine Büning, Hans
AB  - Diese Arbeit präsentiert ein abstraktionsverfeinerungsbasiertes Verifikationsframework für nebenläufige Systeme. Zur Abstraktion verwenden wir eine Kombination aus Prädikatabstraktion und Spotlightabstraktion. Dadurch werden zwei der Hauptursachen der Zustandskomplexität bei der Verifikation nebenläufiger Systeme angegangen. Eine weitere Besonderheit des Verfahrens ist der Einsatz einer 3-wertigen abstrakten Domäne. Eigenschaften in Systemmodellen können die Werte wahr, falsch und unbekannt annehmen, wodurch sich der abstraktionsbedingte Informationsverlust modellieren lässt: Alle wahr- und falsch-Resultate die sich bei der Verifikation ergeben, lassen sich auf das Originalsystem übertragen. Lediglich unbekannt-Resultate erfordern Verfeinerung. Dazu wird auf das Konzept der gegenbeispielgeleiteten Abstraktionsverfeinerung (CEGAR) zurückgegriffen. Gegenbeispiele sind unbekannte Fehlerpfade innerhalb eines Modells. Sie verweisen auf mögliche Verfeinerungsschritte zur Auflösung der Ungewissheit. Dies können neue Prädikate oder Prozesse sein. Typischerweise erweist sich nicht jeder potentielle Verfeinerungsschritt als zielführend, was die Auswahl geeigneter Schritte zu einer schwierigen Aufgabe macht. In dieser Arbeit wird eine Erweiterung des CEGAR-Konzepts eingeführt, basierend auf heuristischer Leitung: Auf Grundlage einer Abstraktionsabhängigkeitsanalyse werden potentielle Verfeinerungsschritte bezüglich des Nutzens für die aktuelle Verifikationsaufgabe heuristisch bewertet und der bestbewertete Schritt wird zur Verfeinerung ausgewählt. Wir zeigen, dass der heuristische Ansatz zu einer signifikanten Leistungssteigerung der Verifikation beitragen kann. Das entwickelte Verfahren erlaubt die Verifikation von CTL Eigenschaften von größenbeschränkten sowie parametrisierten nebenläufigen Systemen.
AU  - Timm, Nils
DA  - 2013
DP  - Universität Paderborn
LA  - eng
N1  - Tag der Verteidigung: 24.06.2013
N1  - Paderborn, Univ., Diss., 2013
PB  - Veröffentlichungen der Universität
PY  - 2013
T2  - Institut für Informatik
TI  - Three-valued abstraction and heuristic-guided refinement for verifying concurrent systems
UR  - https://nbn-resolving.org/urn:nbn:de:hbz:466:2-11773
Y2  - 2026-01-14T08:30:17
ER  -