Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25903
Titel: Model checking with abstraction refinement for well-structured systems
Verfasser: Dimitrova, Rayana
Sprache: Englisch
Erscheinungsjahr: 2006
SWD-Schlagwörter: Abstraktion
Unendlicher Zustandsraum
Verifikation
Freie Schlagwörter: abstraction
verification
infinite-state system
DDC-Sachgruppe: 004 Informatik
Dokumentart : Examensarbeiten (Diplom / Master / Staatsexamen etc.)
Kurzfassung: Abstraction plays an important role in the verification of infinite-state systems. One of the most promising and popular abstraction techniques is predicate abstraction. The right abstraction, i.e. the one that is sufficiently precise to prove or disprove the property under consideration, is automatically constructed by iterative abstraction refinement. The abstract-check-refine loop is not guaranteed to terminate in general. This results in the construction of semi-algorithms that may not terminate on some inputs. For the class of well-structured transition systems, a large class of infinitestate systems, general decidability results hold. These are transition systems equipped with a well-quasi ordering on the set of states which is compatible with the transition relation. In particular coverability, i.e. reachability of an upward-closed set, is known to be decidable for this class of systems. In this work we study the verification of well-structured systems w.r.t. the coverability property by means of predicate abstraction and refinement. We investigate the conditions under which the abstract-check-refine loop is guaranteed to terminate on instances of this class, provide a model checking method based on predicate abstraction and abstraction refinement and prove its completeness for this class of systems.
nicht vorhanden
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-13339
hdl:20.500.11880/25959
http://dx.doi.org/10.22028/D291-25903
SciDok-Publikation: 16-Nov-2007
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
Diplomarbeit_9772_Dimi_Raya_2006.pdf418,35 kBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.