Scalable Techniques for Formal Verification (eBook)
XIV, 243 Seiten
Springer US (Verlag)
978-1-4419-5998-0 (ISBN)
This book is about formal veri?cation, that is, the use of mathematical reasoning to ensure correct execution of computing systems. With the increasing use of c- puting systems in safety-critical and security-critical applications, it is becoming increasingly important for our well-being to ensure that those systems execute c- rectly. Over the last decade, formal veri?cation has made signi?cant headway in the analysis of industrial systems, particularly in the realm of veri?cation of hardware. A key advantage of formal veri?cation is that it provides a mathematical guarantee of their correctness (up to the accuracy of formal models and correctness of r- soning tools). In the process, the analysis can expose subtle design errors. Formal veri?cation is particularly effective in ?nding corner-case bugs that are dif?cult to detect through traditional simulation and testing. Nevertheless, and in spite of its promise, the application of formal veri?cation has so far been limited in an ind- trial design validation tool ?ow. The dif?culties in its large-scale adoption include the following (1) deductive veri?cation using theorem provers often involves - cessive and prohibitive manual effort and (2) automated decision procedures (e. g. , model checking) can quickly hit the bounds of available time and memory. This book presents recent advances in formal veri?cation techniques and d- cusses the applicability of the techniques in ensuring the reliability of large-scale systems. We deal with the veri?cation of a range of computing systems, from - quential programsto concurrentprotocolsand pipelined machines.
Scalable Techniques for Formal Verification 1
Preface 7
Contents 11
1 Introduction 15
Part I Preliminaries 20
2 Overview of Formal Verification 21
2.1 Theorem Proving 21
2.2 Temporal Logic and Model Checking 24
2.3 Program Logics, Axiomatic Semantics, and Verification Conditions 29
2.4 Bibliographic Notes 34
3 Introduction to ACL2 36
3.1 Basic Logic of ACL2 36
3.2 Ground Zero Theory 38
3.2.1 Terms, Formulas, Functions, and Predicates 41
3.2.2 Ordinals and Well-Founded Induction 43
3.3 Extension Principles 46
3.3.1 Definitional Principle 47
3.3.2 Encapsulation Principle 51
3.3.3 Defchoose Principle 53
3.4 The Theorem Prover 55
3.5 Structuring Mechanisms 56
3.6 Evaluators 57
3.7 The ACL2 Programming Environment 58
3.8 Bibliographic Notes 59
Part II Sequential Program Verification 61
4 Sequential Programs 62
4.1 Modeling Sequential Programs 62
4.2 Proof Styles 64
4.2.1 Stepwise Invariants 64
4.2.2 Clock Functions 65
4.3 Comparison of Proof Styles 66
4.4 Verifying Program Components and Generalized Proof Obligations 68
4.5 Discussion 71
4.5.1 Overspecification 71
4.5.2 Forced Homogeneity 72
4.6 Summary 73
4.7 Bibliographic Notes 73
5 Operational Semantics and Assertional Reasoning 74
5.1 Cutpoints, Assertions, and VCG Guarantees 74
5.2 VCG Guarantees and Symbolic Simulation 77
5.3 Composing Correctness Statements 79
5.4 Applications 81
5.4.1 Fibonacci Implementation on TINY 82
5.4.2 Recursive Factorial Implementation on the JVM 84
5.4.3 CBC-Mode Encryption and Decryption 84
5.5 Comparison with Related Approaches 85
5.6 Summary 87
5.7 Bibliographic Notes 87
6 Connecting Different Proof Styles 89
6.1 Soundness of Proof Styles 90
6.2 Completeness 92
6.3 Remarks on Mechanization 96
6.4 Discussion 96
6.5 Summary and Conclusion 98
6.6 Bibliographic Notes 99
Part III Verification of Reactive Systems 101
7 Reactive Systems 102
7.1 Modeling Reactive Systems 103
7.2 Stuttering Trace Containment 104
7.3 Fairness Constraints 106
7.4 Discussion 110
7.5 Summary 113
7.6 Bibliographic Notes 114
8 Verifying Concurrent Protocols Using Refinements 115
8.1 Reduction via Stepwise Refinement 116
8.2 Reduction to Single-Step Theorems 116
8.3 Equivalences and Auxiliary Variables 120
8.4 Examples 122
8.4.1 An ESI Cache Coherence Protocol 122
8.4.2 An Implementation of the Bakery Algorithm 125
8.4.3 A Concurrent Deque Implementation 130
8.5 Summary 135
8.6 Bibliographic Notes 135
9 Pipelined Machines 137
9.1 Simulation Correspondence, Pipelines, and Flushing Proofs 137
9.2 Reducing Flushing Proofs to Refinements 140
9.3 A New Proof Rule 142
9.4 Example 143
9.5 Advanced Features 147
9.5.1 Stalls 147
9.5.2 Interrupts 147
9.5.3 Out-of-Order Execution 148
9.5.4 Out-of-Order and Multiple Instruction Completion 148
9.6 Summary 149
9.7 Bibliographic Notes 150
Part IV Invariant Proving 152
10 Invariant Proving 153
10.1 Predicate Abstractions 155
10.2 Discussion 157
10.3 An Illustrative Example 158
10.4 Summary 160
10.5 Bibliographic Notes 161
11 Predicate Abstraction via Rewriting 162
11.1 Features and Optimizations 166
11.1.1 User-Guided Abstraction 167
11.1.2 Assume Guarantee Reasoning 167
11.2 Reachability Analysis 168
11.3 Examples 169
11.3.1 Proving the ESI 169
11.3.2 German Protocol 171
11.4 Summary and Comparisons 172
11.5 Bibliographic Notes 174
Part V Formal Integration of Decision Procedures 175
12 Integrating Deductive and Algorithmic Reasoning 176
13 A Compositional Model Checking Procedure 179
13.1 Formalizing a Compositional Model Checking Procedure 180
13.1.1 Finite State Systems 180
13.1.2 Temporal Logic formulas 181
13.1.3 Compositional Procedure 181
13.2 Modeling LTL Semantics 183
13.3 Verification 187
13.4 A Deficiency of the Integration and Logical Issues 190
13.5 A Possible Remedy: Integration with HOL4 192
13.6 Summary and Discussion 193
13.7 Bibliographic Notes 194
14 Connecting External Deduction Tools with ACL2 195
14.1 Verified External Tools 196
14.1.1 Applications of Verified External Tools 200
14.1.1.1 Adding a Hypothesis 200
14.1.1.2 Equality Reasoning 201
14.1.1.3 Sorting Bit Vector Addition 202
14.2 Basic Unverified External Tools 203
14.2.1 Applications of Unverified External Tools 204
14.3 Unverified External Tools for Implicit Theories 205
14.4 Remarks on Implementation 209
14.4.1 Basic Design Decisions 209
14.4.2 Miscellaneous Engineering Considerations 211
14.5 Summary 214
14.6 Bibliographic Notes 215
Part VI Conclusion 217
15 Summary and Conclusion 218
References 221
Index 235
| Erscheint lt. Verlag | 17.6.2010 |
|---|---|
| Zusatzinfo | XIV, 243 p. |
| Verlagsort | New York |
| Sprache | englisch |
| Themenwelt | Informatik ► Weitere Themen ► CAD-Programme |
| Technik ► Elektrotechnik / Energietechnik | |
| Technik ► Nachrichtentechnik | |
| Schlagworte | Algorithmic reasoning • algorithms • Computer • Computer-Aided Reasoning • design automation • Electronic Design Automation • Embedded Systems • formal methods • Formal Verification • Model • Model Checking • theorem proving • verification |
| ISBN-10 | 1-4419-5998-X / 144195998X |
| ISBN-13 | 978-1-4419-5998-0 / 9781441959980 |
| Haben Sie eine Frage zum Produkt? |
PDF (Wasserzeichen)Größe: 2,1 MB
DRM: Digitales Wasserzeichen
Dieses eBook enthält ein digitales Wasserzeichen und ist damit für Sie personalisiert. Bei einer missbräuchlichen Weitergabe des eBooks an Dritte ist eine Rückverfolgung an die Quelle möglich.
Dateiformat: PDF (Portable Document Format)
Mit einem festen Seitenlayout eignet sich die PDF besonders für Fachbücher mit Spalten, Tabellen und Abbildungen. Eine PDF kann auf fast allen Geräten angezeigt werden, ist aber für kleine Displays (Smartphone, eReader) nur eingeschränkt geeignet.
Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen dafür einen PDF-Viewer - z.B. den Adobe Reader oder Adobe Digital Editions.
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen dafür einen PDF-Viewer - z.B. die kostenlose Adobe Digital Editions-App.
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.
aus dem Bereich
