A lattice-theoretic framework for circular assume-guarantee reasoning [Elektronische Ressource] / von Patrick Maier

A Lattice-Theoretic FrameworkFor Circular Assume-GuaranteeReasoningDissertationzur Erlangung des GradesDoktor der Ingenieurwissenschaften (Dr.-Ing.)der Naturwissenschaftlich-Technischen Fakult¨at Ider Universit¨at des SaarlandesvonPatrick MaierSaarbruc¨ ken2003Tag des Kolloquiums: 23. Juli 2003Dekan: Prof. Dr.-Ing. Philipp SlusallekBerichterstatter: Prof. Dr. Harald GanzingerProf. Dr. Andreas PodelskiSriram K. Rajamani, Ph.D.KurzzusammenfassungWir entwickeln einen abstrakten verbandstheoretischen Rahmen in dem wir dieKorrektheit und andere Eigenschaften bedingter zirkular¨ er Assume-Guarantee-Regeln(A-G-Regeln)untersuchen.WirisoliereneinebesondereNebenbedingung,non-blockingness, die zu einem verst¨andlichen induktiven Beweis der Korrekt-heit zirkularer A-G-Regeln fuhrt. Ausserdem sind durch non-blockingness ein-¨ ¨geschrank¨ te zirkular¨ e Regeln vollstandig¨ und star¨ ker als eine grosse Klasse vonkorrekten bedingten A-G-Regeln. So gesehen erhellt unsere Arbeit die Grundla-gen des zirkularen A-G-Paradigmas.¨AufgrundseinerAbstraktheitkannunserRahmenzuvielenkonkretenForma-lismen instanziiert werden. Wir zeigen, dass mehrere bekannte A-G-Regeln zurkompositionalen Verifikation Instanzen unserer generischen Regeln sind. So istder zirkularitatsauflosende Beweis der Korrektheit nur einmal fur unsere gene-¨ ¨ ¨rische Regeln zu fuhren,¨ dann erben alle Instanzen Korrektheit, ohne dass nocheinmal ein zirkularitatsauflosender Beweis notig ist.