Embedded Software Verification and Debugging (eBook)

Djones Lettnin, Markus Winterholer (Herausgeber)

eBook Download: PDF

2017 | 1. Auflage
XVI, 220 Seiten
Springer New York (Verlag)
978-1-4614-2266-2 (ISBN)

Infos

This book provides comprehensive coverage of verification and debugging techniques for embedded software, which is frequently used in safety critical applications (e.g., automotive), where failures are unacceptable.  Since the verification of complex systems needs to encompass the verification of both hardware and embedded software modules, this book focuses on verification and debugging approaches for embedded software with hardware dependencies.  Coverage includes the entire flow of design, verification and debugging of embedded software and all key approaches to debugging, dynamic, static, and hybrid verification.  This book discusses the current, industrial embedded software verification flow, as well as emerging trends with focus on formal and hybrid verification and debugging approaches.

Markus Winterholer has been involved in system design and HW/SW development for more than 20 years. Most recently he has been focused on developing and testing software for the financial sector and e-government solutions in Switzerland. Before, he was responsible for the development of several generations of embedded software debug and verification solutions at Cadence for more than ten years. Furthermore, he also deployed advanced verification methodologies including application of constrained random techniques. Before he joined Cadence, he worked five years as a freelancer offering consulting services for hardware and software development and verification focusing on leading edge communication standards and processors. Markus Winterholer holds a diploma degree in computer science from the University of Tübingen.

Djones Lettnin has a Master's in Electric Engineering at the Catholic University of Rio Grande do Sul (2004), Brazil, and a PhD. in Computer Engineering at the Eberhard Karls University of Tübingen (2009), Germany. Since August 2011, he has been a Professor at Federal University of Santa Catarina, Brazil. He works in many cooperation projects with Cadence Design Systems, Freescale, Bosch, and Intel. He is also the coordinator of the Cadence Academic Network in Latin America. His main interests are in design and functional verification of hardware and embedded software with a main focus on: EDA, modeling of embedded systems, digital design, verification based on assertions, and semiformal and formal verification using model checking.

Inhalt

Foreword 7
Contents 9
Contributors 14
1 An Overview About Debugging and Verification Techniques for Embedded Software 16
1.1 The Importance of Debugging and Verification Processes 16
1.2 Debugging and Verification Platforms 19
1.2.1 OS Simulation 19
1.2.2 Virtual Platform 20
1.2.3 RTL Simulation 20
1.2.4 Acceleration/Emulation 20
1.2.5 FPGA Prototyping 21
1.2.6 Prototyping Board 21
1.2.7 Choosing the Right Platform for Software Development and Debugging 22
1.3 Debugging Methodologies 22
1.3.1 Interactive Debugging 23
1.3.2 Post-Process Debugging 23
1.3.3 Choosing the Right Debugging Methodology 25
1.4 Verification Methodologies 25
1.4.1 Verification Planning 25
1.4.2 Verification Environment Development 26
1.5 Summary 29
References 30
2 Embedded Software Debug in Simulation and Emulation Environments for Interface IP 34
2.1 Firmware Debug Methods Overview 34
2.2 Firmware Debuggability 37
2.3 Test-Driven Firmware Development for Interface IP 39
2.3.1 Starting Development 39
2.3.2 First Functional Tests 42
2.3.3 Debugging a System 46
2.3.4 System Performance 48
2.3.5 Interface IP Performance in a Full Featured OS Case 49
2.3.6 Low Level Firmware Debug in a State-of-the-Art Embedded System 50
2.4 Firmware Bring-up as a Hardware Verification Tool 50
2.4.1 NAND Flash 50
2.4.2 xHCI 51
2.5 Playback Debugging with Cadence® Indago’ Embedded Software Debugger 53
2.5.1 Example 54
2.5.2 Coverage Measurement 57
2.5.3 Drawbacks 59
2.6 Conclusions 59
References 60
3 The Use of Dynamic Temporal Assertions for Debugging 61
3.1 Introduction 61
3.1.1 DTA Assertions Versus Ordinary Assertions 62
3.1.2 DTA Assertions Versus Conditional Breakpoints 64
3.2 Debugging with DTA Assertions 64
3.3 Design 65
3.3.1 Past-Time DTA Assertions 67
3.3.2 Future-Time DTA Assertions 67
3.3.3 All-Time DTA Assertions 68
3.4 Assertion's Evaluation 68
3.4.1 Temporal Cycles and Limits 70
3.4.2 Evaluation Log 71
3.4.3 DTA Assertions and Atomic Agents 71
3.5 Implementation 73
3.6 Evaluation 74
3.6.1 Performance 75
3.7 Challenges and Future Work 76
3.8 Conclusion 77
References 78
4 Automated Reproduction and Analysis of Bugs in Embedded Software 80
4.1 Introduction 80
4.2 Overview 82
4.3 Debugger-Based Bug Reproduction 83
4.3.1 State of the Art 84
4.3.2 Theory and Algorithms 86
4.3.3 Implementation 88
4.3.4 Experiments 91
4.4 Dynamic Verification During Replay 93
4.4.1 State of the Art 93
4.4.2 Theory and Workflow 94
4.4.3 Implementation of Assertions During Replay 95
4.4.4 Experiments 96
4.5 Root-Cause Analyses 97
4.5.1 State of the Art 98
4.5.2 Theory and Concepts 99
4.5.3 Implementation 110
4.5.4 Experiments 113
4.6 Summary 117
References 117
5 Model-Based Debugging of Embedded Software Systems 120
5.1 Introduction 120
5.1.1 Problem Statement 121
5.1.2 Contribution 122
5.2 Related Work 123
5.3 Model-Based Debugging Framework 125
5.3.1 Overview 125
5.4 Runtime Monitoring 129
5.4.1 Classification of Runtime Monitoring 129
5.4.2 Time-and Memory-Aware Runtime Monitoring Approaches 131
5.5 Experimental Evaluation 132
5.5.1 Software Monitoring 132
5.5.2 On-Chip (Software) Monitoring 136
5.6 Performance Metrics 138
5.6.1 Software Monitoring 138
5.6.2 On-Chip (Software) Monitoring 141
5.7 Discussion and Evaluation 142
5.7.1 Salient Features in the Proposed Approach 143
5.8 Conclusion 144
References 144
6 A Mechanism for Monitoring Driver-Device Communication 146
6.1 Introduction 146
6.2 Related Works 148
6.3 Proposed Approach 149
6.4 Definition of the HFSM-D State Machine 154
6.5 The TDevC Language 157
6.5.1 TDevC Device Model 157
6.5.2 TDevC Platform Model 163
6.6 Architecture of the Monitoring Module 165
6.7 Experiments and Results 166
6.8 Conclusions 169
6.8.1 Future Works 169
References 170
7 Model Checking Embedded C Software Using k-Induction and Invariants 172
7.1 Introduction 172
7.2 Motivating Example 174
7.3 Induction-Based Verification of C Programs Using Invariants 175
7.3.1 The Proposed k-Induction Algorithm 175
7.3.2 Running Example 180
7.4 Experimental Evaluation 185
7.4.1 Experimental Setup 185
7.4.2 Experimental Results 186
7.5 Related Work 192
7.6 Conclusions 193
References 194
8 Scalable and Optimized Hybrid Verification of Embedded Software 196
8.1 Introduction 196
8.2 Related Work 197
8.2.1 Contributions 199
8.3 VERIFYR Verification Methodology 199
8.3.1 SPA Heuristic 202
8.3.2 Preprocessing Phase 204
8.3.3 Orchestrator 207
8.3.4 Coverage 208
8.3.5 Technical Details 208
8.4 Results and Discussion 210
8.4.1 Testing Environment 210
8.4.2 Motorola Powerstone Benchmark Suite 210
8.4.3 Verification Results Using VERIFYR 212
8.4.4 EEPROM Emulation Software from NEC Electronics 213
8.5 Conclusion and Future Work 216
References 216
Index 219

Produkt-Details

• Erscheint lt. Verlag: 17.4.2017
• Reihe/Serie: Embedded Systems
• Zusatzinfo: XVI, 208 p. 80 illus., 62 illus. in color.
• Verlagsort: New York
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Software Entwicklung
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• Themenwelt: Technik ► Elektrotechnik / Energietechnik
• Schlagworte: Dynamic Testing • dynamic verification • Embedded Software • Embedded Software Debugging • Embedded Software Design • Embedded Software Testing • embedded software verification • Embedded Systems • Integrated Circuits • Static and Hybrid Verification
• ISBN-10: 1-4614-2266-3 / 1461422663
• ISBN-13: 978-1-4614-2266-2 / 9781461422662