SciDok

Eingang zum Volltext in SciDok

Hinweis zum Urheberrecht

Diplomarbeit, Magisterarbeit zugänglich unter
URN: urn:nbn:de:bsz:291-scidok-13339
URL: http://scidok.sulb.uni-saarland.de/volltexte/2007/1333/


Model checking with abstraction refinement for well-structured systems

Dimitrova, Rayana

pdf-Format:
Dokument 1.pdf (418 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Abstraktion , Unendlicher Zustandsraum , Verifikation
Freie Schlagwörter (Englisch): abstraction , verification , infinite-state system
Institut: Fachrichtung 6.2 - Informatik
DDC-Sachgruppe: Informatik
Dokumentart: Diplomarbeit, Magisterarbeit
Sprache: Englisch
Erstellungsjahr: 2006
Publikationsdatum: 16.11.2007
Kurzfassung auf Englisch: 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.
Kurzfassung auf Deutsch: nicht vorhanden

Home | Impressum | Über SciDok | Policy | Kontakt | Datenschutzerklärung | English