Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25787
Titel: A lattice-theoretic framework for circular assume-guarantee reasoning
Verfasser: Maier, Patrick
Sprache: Englisch
Erscheinungsjahr: 2003
SWD-Schlagwörter: Gittertheorie
Freie Schlagwörter: lattice - theoretic framework; circular assume-guarantee rules
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: We develop an abstract lattice-theoretic framework within which we study soundness and other properties of circular assume-guarantee (A-G) rules constrained by side conditions. We identify a particular side condition, non-blockingness, which admits an intelligible inductive proof of the soundness of circular A-G reasoning. Besides, conditional circular rules based on non-blockingness turn out to be complete in various senses and stronger than a large class of sound conditional A-G rules. In this respect, our framework enlightens the foundations of circular A-G reasoning. Due to its abstractness, the framework can be instantiated to many concrete settings. We show several known circular A-G rules for compositional verification to be instances of our generic rules. Thus, we do the circularity-breaking inductive argument once to establish soundness of our generic rules, which then implies soundness of all the instances without resorting to technically complicated circularity-breaking arguments for each single rule. In this respect, our framework unifies many approaches to circular A-G reasoning and provides a starting point for the systematic development of new circular A-G rules.
Wir entwickeln einen abstrakten verbandstheoretischen Rahmen in dem wir die Korrektheit und andere Eigenschaften bedingter zirkulaerer Assume-Guarantee- Regeln (A-G-Regeln) untersuchen. Wir isolieren eine besondere Nebenbedingung, non-blockingness, die zu einem verstaendlichen induktiven Beweis der Korrektheit zirkulaerer A-G-Regeln fuehrt. Ausserdem sind durch non-blockingness eingeschr aenkte zirkulaere Regeln vollstaendig und staerker als eine grosse Klasse von korrekten bedingten A-G-Regeln. So gesehen erhellt unsere Arbeit die Grundlagen des zirkulaeren A-G-Paradigmas.Aufgrund seiner Abstraktheit kann unser Rahmen zu vielen konkreten Formalismen instanziiert werden. Wir zeigen, dass mehrere bekannte A-G-Regeln zur kompositionalen Verifikation Instanzen unserer generischen Regeln sind. So ist der zirkularitaetsaufloesende Beweis der Korrektheit nur einmal fuer unsere generische Regeln zu fuehren, dann erben alle Instanzen Korrektheit, ohne dass noch einmal ein zirkularitaets-aufloesender Beweis noetig ist. In dieser Hinsicht stellt unser Rahmen eine einheitliche Plattform dar, die verschiedene Ausformungen des zirkulaeren A-G-Paradigmas umfasst und von der ausgehend systematisch neue zirkulaere A-G-Regeln entwickelt werden koennen.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-3267
hdl:20.500.11880/25843
http://dx.doi.org/10.22028/D291-25787
Erstgutachter: Harald Ganzinger
Tag der mündlichen Prüfung: 23-Jul-2003
SciDok-Publikation: 9-Aug-2004
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 
PatrickMaier_ProfDrHaraldGanzinger.pdf665,08 kBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.