Lettnin / Winterholer Embedded Software Verification and Debugging

1. Auflage 2017
ISBN: 978-1-4614-2266-2
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 220 Seiten

Reihe: Embedded Systems

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.

Autoren/Hrsg.

Lettnin, Djones

Winterholer, Markus

Inhaltsverzeichnis

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