New techniques for abstraction refinement

Abstract: Abstraction refinement refers to the automatic construction of an abstract model from a model of a system. The goal is to obtain an abstract model that is amenable to model checking methods. The motivation for this thesis lies in the observation that the pivotal point of model checking is the construction of a suitable abstract model from the original model. If the abstract model is a too coarse abstraction of the given model of the system, the abstract model no longer satisfies the given correctness property even though the original model does. In this case, the abstraction needs to be refined. In the CEGAR scheme, the abstraction is refined based on a spurious counterexample. A spurious counterexample is an execution which is admitted by the abstract model but not by the original model. This process of counterexample-guided abstraction refinement is iterated until the abstract model satisfies the given correctness property or no spurious counterexample exists.

This thesis presents new techniques to construct new abstractions from spurious counterexamples for the case of software systems and for the case of cyber-physical systems. The ideas for the new techniques stem from fields as diverse as abstract interpretation, assume-guarantee reasoning, and linear optimization. For each abstraction refinement technique, we present an implementation and an experimental evaluation which shows the practical potential of the respective technique
Abstract: Abstraktionsverfeinerung beschreibt ein Verfahren zur automatischen Konstruktion eines abstrakten Modells für ein Systemmodell. Ziel ist es, ein abstraktes Modell zu erhalten, welches sich für das Anwenden von Model-Checking-Methoden eignet. Die Motivation dieser Arbeit entstammt der Beobachtung, dass die Konstruktion eines passenden abstrakten Modells für das Originalmodell ausschlaggebend für die Durchführbarkeit von Model-Checking-Methoden ist. Wenn das abstrakte Modell eine zu grobe Abstraktion des Systemmodells darstellt, wird die gegebene Korrektheitseigenschaft nicht mehr vom abstrakten Modell erfüllt, obwohl sie vom originalen Systemmodell erfüllt wird. In diesem Fall muss das abstrakte Modell verfeinert werden. Im CEGAR Schema wird die Abstraktion basierend auf einem unechten Gegenbeispiel verfeinert. Ein unechtes Gegenbeispiel entspricht einer zulässigen Ausführung im abstrakten Modell, welche jedoch im Originalmodell unzulässig ist. Dieses Verfahren zur Abstraktionsverfeinerung, welches auf unechten Gegenbeispielen basiert, wird so lange wiederholt, bis das abstrakte Modell die gegebene Korrektheitseigenschaft erfüllt, oder kein unechtes Gegenbeispiel existiert.

Diese Arbeit präsentiert neue Techniken, um neue Abstraktionen mit Hilfe von unechten Gegenbeispielen zu konstruieren. Hierbei werden Softwaresysteme und cyber-physische Systeme betrachtet. Die Ideen, auf denen die neuen Techniken basieren, stammen aus Bereichen wie abstrakter Interpretation, Assume-Guarantee-Reasoning und linearer Optimierung. Zu jeder Abstraktionsverfeinerungstechnik werden eine Implementierung und eine experimentelle Auswertung vorgestellt, die das praktische Potenzial der jeweiligen Technik verdeutlichen

Angaben zum Objekt

• Standort: Deutsche Nationalbibliothek Frankfurt am Main
• Umfang: Online-Ressource
• Sprache: Englisch
• Anmerkungen: Universität Freiburg, Dissertation, 2018

Beteiligte, Orts- und Zeitangaben

• Ereignis: Veröffentlichung
• (wo): Freiburg
• (wer): Universität
• (wann): 2018
• Urheber: Greitschus, Marius
• Beteiligte Personen und Organisationen: Podelski, Andreas ; Albert-Ludwigs-Universität Freiburg. Fakultät für Angewandte Wissenschaften

Weitere Informationen

• DOI: 10.6094/UNIFR/17100
• URN: urn:nbn:de:bsz:25-freidok-171004
• Rechteinformation: Kein Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
• Letzte Aktualisierung: 14.08.2025, 11:03 MESZ