Please use this identifier to cite or link to this item:
doi:10.22028/D291-25903
Title: | Model checking with abstraction refinement for well-structured systems |
Author(s): | Dimitrova, Rayana |
Language: | English |
Year of Publication: | 2006 |
SWD key words: | Abstraktion Unendlicher Zustandsraum Verifikation |
Free key words: | abstraction verification infinite-state system |
DDC notations: | 004 Computer science, internet |
Publikation type: | Other |
Abstract: | 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 to this record: | urn:nbn:de:bsz:291-scidok-13339 hdl:20.500.11880/25959 http://dx.doi.org/10.22028/D291-25903 |
Date of registration: | 16-Nov-2007 |
Faculty: | MI - Fakultät für Mathematik und Informatik |
Department: | MI - Informatik |
Collections: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Files for this record:
File | Description | Size | Format | |
---|---|---|---|---|
Diplomarbeit_9772_Dimi_Raya_2006.pdf | 418,35 kB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.