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

Sujets

• Informatik

Informations

• Publié par: universitat_des_saarlandes
• Publié le: 01 janvier 2004
• Nombre de lectures: 16
• Langue: Deutsch

Extrait

A Lattice-Theoretic Framework
For Circular Assume-Guarantee
Reasoning
Dissertation
zur Erlangung des Grades
Doktor der Ingenieurwissenschaften (Dr.-Ing.)
der Naturwissenschaftlich-Technischen Fakult¨at I
der Universit¨at des Saarlandes
von
Patrick Maier
Saarbruc¨ ken
2003Tag des Kolloquiums: 23. Juli 2003
Dekan: Prof. Dr.-Ing. Philipp Slusallek
Berichterstatter: Prof. Dr. Harald Ganzinger
Prof. Dr. Andreas Podelski
Sriram K. Rajamani, Ph.D.Kurzzusammenfassung
Wir entwickeln einen abstrakten verbandstheoretischen Rahmen in dem wir die
Korrektheit 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 von
korrekten 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 zur
kompositionalen Verifikation Instanzen unserer generischen Regeln sind. So ist
der zirkularitatsauflosende Beweis der Korrektheit nur einmal fur unsere gene-¨ ¨ ¨
rische Regeln zu fuhren,¨ dann erben alle Instanzen Korrektheit, ohne dass noch
einmal ein zirkularitatsauflosender Beweis notig ist. In dieser Hinsicht stellt un-¨ ¨ ¨
ser Rahmen eine einheitliche Plattform dar, die verschiedene Ausformungen des
zirkular¨ en A-G-Paradigmas umfasst und von der ausgehend systematisch neueare A-G-Regeln entwickelt werden konnen.¨ ¨Abstract
Wedevelopanabstractlattice-theoreticframeworkwithinwhichwestudysound-
nessandotherpropertiesofcircularassume-guarantee(A-G)rulesconstrainedby
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 com-
plete 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 verifica-
tion 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
impliessoundnessofalltheinstanceswithoutresortingtotechnicallycomplicated
circularity-breaking arguments for each single rule. In this respect, our frame-
work unifies many approaches to circular A-G reasoning and provides a starting
point for the systematic development of new circular A-G rules.Acknowledgments
First and foremost I would like to thank Prof. Dr. Harald Ganzinger for accept-
ing me as a PhD student in his group at the Max-Planck-Institut fur¨ Informatik.
Even more I owe him for his continued support and interest in my work, which
showed up the form of brilliant questions. There is no answer without a ques-
tion — many of the ideas in this thesis emerged while thinking about Harald’s
questions.
I was most fortunate to have Prof. Dr. Andreas Podelski as my advisor. He
encouraged my interest in circular assume-guarantee reasoning. I thank him for
manyfruitfuldiscussions,forhispatienceandforteachingmesimpleandeffective
rules how to write.
I am grateful to Dr. Sriram Rajamani for his instant commitment to become
a referee of this thesis.
I am indebted to Dr. Friedrich Eisenbrand, Prof. Dr. Andreas Podelski and
Dr. Emil Weydert for reading drafts of the introduction. I owe immense grat-
itude to Dr. Viorica Sofronie-Stokkermans and Dr. Uwe Waldmann for reading
drafts of the thesis in great detail and providing me with valuable comments and
corrections.
Over the years there were a number of colleagues who were always willing to
discuss a problem. The ones I recall are Werner Backes, Dr. Witold Charatonik,
Dr. Giorgio Delzanno, Dr. Friedrich Eisenbrand, Lilia Georgieva, Thomas Hillen-
brand, Dr. Manfred Jaeger, Dr. Hans de Nivelle, Andrey Rybalchenko, Dr. Vior-
ica Sofronie-Stokkermans, Dr. Jurgen¨ Stuber, Dr. Jean-Marc Talbot, Dr. Uwe
Waldmann and Dr. Emil Weydert. Apologies to those I have forgotten.
Special thanks go to Lilia for providing emotional support in hard times.Contents
Zusammenfassung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
Extended Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1 Introduction 7
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2 Outline. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2 Preliminaries 17
2.1 Ordered Sets, Semilattices, Lattices, etc. . . . . . . . . . . . . . . 17
2.2 Some Examples of Ordered Sets . . . . . . . . . . . . . . . . . . . 21
3 Inferences in Semilattices 25
3.1 Terms, Formulas and Relations . . . . . . . . . . . . . . . . . . . 25
3.2 Satisfiability and Entailment . . . . . . . . . . . . . . . . . . . . . 28
3.3 Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.4 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.5 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.6 Assume-Guarantee Rules . . . . . . . . . . . . . . . . . . . . . . . 41
4 The Framework 47
4.1 Well-founded Approximations . . . . . . . . . . . . . . . . . . . . 48
4.2 Non-Blockingness . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.3 The Basic Circular Assume-Guarantee Rule . . . . . . . . . . . . 53
4.4 Extension To More Than Two Properties . . . . . . . . . . . . . . 55
4.5 Another Extension . . . . . . . . . . . . . . . . . . . . . . . . . . 61
4.6 Compositional Assume-Guarantee Rules . . . . . . . . . . . . . . 62
4.7 Beyond Well-founded Approximations . . . . . . . . . . . . . . . . 65
5 Instantiations 69
5.1 Rules For Moore Machines . . . . . . . . . . . . . . . . . . . . . . 71
5.1.1 Moore Machines. . . . . . . . . . . . . . . . . . . . . . . . 71
5.1.2 Linear-Time Semantics . . . . . . . . . . . . . . . . . . . . 73
5.1.3 Branching-Time Semantics . . . . . . . . . . . . . . . . . . 815.1.4 Comparison to Other Work . . . . . . . . . . . . . . . . . 88
5.2 Rules for Assume-Guarantee Specifications . . . . . . . . . . . . . 92
5.2.1 (Linear-Time) Behaviors And Properties . . . . . . . . . . 92
5.2.2 Implication . . . . . . . . . . . . . . . . . . . . . . . . . . 94
5.2.3 Safety And Liveness . . . . . . . . . . . . . . . . . . . . . 96
5.2.4 Assume-Guarantee Specifications . . . . . . . . . . . . . . 99
5.2.5 Asuarantee Rules . . . . . . . . . . . . . . . . . . . 101
5.2.6 Comparison to Other Work . . . . . . . . . . . . . . . . . 106
Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
List of Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117