Embedded Systems and Software Validation (eBook)

Front Cover 1
Embedded Systems and Software Validation 4
Copyright Page 5
Dedication Page 6
Table of Contents 8
Acknowledgments 10
Preface 12
Chapter 1. Introduction 14
Chapter 2. Model Validation 20
2.1 Platform versus System Behavior 21
2.2 Criteria for Design Model 23
2.3 Informal Requirements: A Case Study 25
2.3.1 The Requirements Document 26
2.3.2 Simplification of the Informal Requirements 27
2.4 Common Modeling Notations 29
2.4.1 Finite-State Machines 29
2.4.2 Communicating FSMs 33
2.4.3 Message Sequence Chart–Based Models 40
2.5 Remarks About Modeling Notations 50
2.6 Model Simulations 52
2.6.1 FSM Simulations 54
2.6.2 Simulating MSC-Based System Models 59
2.7 Model-Based Testing 63
2.8 Model Checking 71
2.8.1 Property Specification 71
2.8.2 Checking Procedure 86
2.9 The SPIN Validation Tool 95
2.10 The SMV Validation Tool 99
2.11 Case Study: Air-Traffic Controller 102
2.12 References 104
2.13 Exercises 106
Chapter 3. Communication Validation 108
3.1 Common Incompatibilities 111
3.1.1 Sending/Receiving Signals in Different Order 112
3.1.2 Handling a Different Signal Alphabet 113
3.1.3 Mismatch in Data Format 115
3.1.4 Mismatch in Data Rates 118
3.2 Converter Synthesis 119
3.2.1 Representing Native Protocols and Converters 119
3.2.2 Basic Ideas for Converter Synthesis 121
3.2.3 Various Strategies for Protocol Conversion 128
3.2.4 Avoiding No-Progress Cycles 129
3.2.5 Speculative Transmission to Avoid Deadlocks 131
3.3 Changing a Working Design 134
3.4 References 135
3.5 Exercises 136
Chapter 4. Performance Validation 138
4.1 The Conventional Abstraction of Time 139
4.2 Predicting Execution Time of a Program 144
4.2.1 WCET Calculation 146
4.2.2 Modeling of Microarchitecture 158
4.3 Interference within a Processing Element 167
4.3.1 Interrupts from Environment 168
4.3.2 Contention and Preemption 170
4.3.3 Sharing a Processor Cache 174
4.4 System-Level Communication Analysis 178
4.5 Designing Systems with Predictable Timing 182
4.5.1 Scratchpad Memories 182
4.5.2 Time-Triggered Communication 187
4.6 Emerging Applications 189
4.7 References 190
4.8 Exercises 190
Chapter 5. Functionality Validation 194
5.1 Dynamic or Trace-Based Checking 197
5.1.1 Dynamic Slicing 200
5.1.2 Fault Localization 209
5.1.3 Directed Testing Methods 216
5.2 Formal Verification 220
5.2.1 Predicate Abstraction 224
5.2.2 Software Checking via Predicate Abstraction 231
5.2.3 Combining Formal Verification with Testing 238
5.3 References 242
5.4 Exercises 243
Bibliography 246
Index 254