Software Verification and Analysis (eBook)

An Integrated, Hands-On Approach

Janusz Laski, William Stanley (Autoren)

eBook Download: PDF

2009 | 1. Auflage
XVIII, 229 Seiten
Springer London (Verlag)
978-1-84882-240-5 (ISBN)

Infos

This book addresses the most important techniques in improving the correctness of software, including correctness by construction (top-down refinement), program proving, static analysis and dynamic, execution-based analysis (testing and debugging). Three major software verification techniques are discussed: Semantic program synthesis and analysis, static program analysis and dynamic program analysis. The correctness by construction paradigm is illustrated using the VDM-SL and the corresponding CSK Toolbox. The discussion involves the synthesis of direct and/or indirect specification, interpreting the latter and carrying out high-level testing of the specification. Problems are included in the text and one or more difficult exercises appear at the end of each chapter. Also, where appropriate, STAD’s handling of the concepts is illustrated. Written for advanced students and professionals wishing to explore more than one technique, this comprehensive text will be invaluable with its unique integrated approach.

---

"e;The situation is good, but not hopeless"e; (Polish folk wisdom) The text is devoted to the Software Analysis and Testing (SAT) methods and s- porting tools for assessing and, if possible, improving software quality, specifically its correctness. The term quality assurance is avoided for it is this author's firm belief that in the current state of the art that goal is unattainable, a plethora of "e;gu- anteed"e; solutions to the problem notwithstanding. Therefore, the rather awkward phrase "e;improving correctness"e; is to be understood as an effort to minimize the number of residual programming faults ("e;bugs"e;) and their impact on the software's behavior, that is, to make the faults tolerable. It is clear that such a minimalist approach is a result of frustration. Indeed, having spent years developing software and teaching (preaching?) "e;How to do it right,"e; I still do not know how to go about it with any degree of certainty! It appears then I probably should stop right now, for who with a modicum of common sense would reach for a text that does not offer salvation but (as will be seen) hard work and misery? If I intend to continue, it is only that I suspect there are many professionals out there who have similar doubts. And they are the intended audience of this project. The philosophical underpinning of the text is the importance of sound engine- ing practices in software development.

Inhalt

Preface 6
Structure of the Text 7
Software Tools 9
The Accompanying Web Site 9
The Audience of the Book 10
Acknowledgments 11
Contents 12
Introduction: What Do We Want To Know About the Program? 16
1 What is the Program Doing: Specification 16
2 How to Make Sure That the Program is Doing it Right: Verification 20
3 Trying to Show That the Program is Incorrect: Testing 23
4 Trying to Locate the Cause of Incorrectness: Debugging 26
5 What One Can Tell About The Program Without Executing It: Static Analysis 30
6 The Scope of the SAT Methods 32
7 Conclusions 35
Exercises 36
References 36
The Semantic Analysis 37
Why Not Write Correct Software the First Time? 38
1.1 Express Yourself Precisely: The Precondition 38
1.2 The Postcondition 41
1.3 The Principles of Top-Down Refinement 45
1.4 The Example Continued 46
1.5 Conclusions 49
References 50
How to Prove a Program Correct: Programs Without Loops 52
2.1 Program Correctness 52
2.2 The Weakest Precondition wp( S , Q) 55
2.3 Finding the wp( S , Q ) 56
2.4 SPARK Experiments 58
2.5 Programs With Many Paths 62
2.6 The Derivation of Partial Weakest Precondition (pwp) and Path Traversal ( tr) 65
2.7 The Assertion Method 69
2.8 Conclusions 73
References 74
How to Prove a Program Correct: Iterative Programs 75
3.1 When You Cannot Verify All Paths: Programs with Loops 75
3.2 From the Particular to the General: Mathematical Induction 77
3.3 Loop Invariants 78
3.4 Where Do Invariants Come From: Goal Invariant 82
3.5 Supporting the Proof: Using the Proof Checker 84
3.6 Does the Loop Terminate? Variants 88
3.7 Conclusions 89
References 91
Prepare Test for Any Implementation: Black- Box Testing 92
4.1 Testing Principles 92
4.2 Functionality Testing 96
4.3 Partition Testing 99
4.4 An Example 100
4.5 Random Testing 106
4.6 Conclusions 108
References 110
Static Analysis 111
Intermediate Program Representation 112
5.1 Introduction 112
5.2 Program Parse and Syntax Trees 113
5.3 Program Control Flowgraph 113
5.4 Labeled Flowgraphs 118
5.5 Deriving the Flowgraph 121
5.6 Paths in Flowgraphs 125
5.7 Conclusions 132
References 132
Program Dependencies 133
6.1 Motivations 133
6.2 Dominators and Attractors 136
6.3 Control Dependency: Structured Control 139
6.4 Control Dependency: Arbitrary Control 143
6.5 Computing Control Dependency 145
6.6 Data and General Dependency 147
6.7 Conclusions 149
References 150
What Can One Tell About a Program Without Its Execution: Static Analysis 151
7.1 Motivations 151
7.2 Control Flow Anomalies 153
7.3 Data Flow Anomalies 155
7.4 Modeling Procedure Calls 160
7.5 Signature Anomalies 166
7.6 Descriptive Static Analysis 171
7.7 Events on Program Paths 173
7.8 Conclusions 176
References 177
Dynamic Analysis 178
Is There a Bug in the Program? Structural Program Testing 179
8.1 Introduction 179
8.2 Code Coverage Criteria 180
8.3 Testing Scenario 185
8.4 Faults and Errors 191
8.5 Fault Detection Power of Code Coverage Testing 197
8.6 Program Dependencies in Software Testing 199
8.7 Conclusions 204
References 207
Dynamic Program Analysis 209
9.1 Introduction 209
9.2 Operational Semantics: States and Computations 210
9.3 Dynamic Analysis Concepts 214
9.4 An Application: Dynamic Program Slicing 217
9.5 An Application: Handling Dynamic Data Structures 220
9.6 Conclusions 223
References 225
Index 226

Produkt-Details

• Erscheint lt. Verlag: 29.4.2009
• Sprache: englisch
• Themenwelt: Informatik ► Software Entwicklung ► Qualität / Testen
• Schlagworte: Debugging • Program dependencies • Program proving • Software • Software Verification • Static Analysis • Testing • verification
• ISBN-10: 1-84882-240-5 / 1848822405
• ISBN-13: 978-1-84882-240-5 / 9781848822405