Laski. / Stanley Software Verification and Analysis

An Integrated, Hands-On Approach
1. Auflage 2009
ISBN: 978-1-84882-240-5
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 229 Seiten

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.

Autoren/Hrsg.

Laski, Janusz

Stanley, William

Inhaltsverzeichnis

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