Embedded systems and software validation / Abhik Roychoudhury.

Format:

Book

Author/Creator:

Roychoudhury, Abhik.

Contributor:

Anne and Joseph Trachtman Memorial Book Fund.

Series:

Morgan Kaufmann series in systems on silicon

The Morgan Kaufmann series in systems on silicon

Language:

English

Subjects (All):

Embedded computer systems--Design and construction.

Embedded computer systems.

Embedded computer systems--Testing.

Computer software--Testing.

Computer software.

Physical Description:

xii, 254 pages : illustrations ; 25 cm.

Place of Publication:

Amsterdam ; Boston : Morgan Kaufmann Publishers/Elsevier, [2009]

Summary:

Roychoudhury offers readers practical debugging and validation techniques for the entire life cycle of embedded systems design.

Modern embedded systems are a part of every modern electronic device, ranging from toys to traffic lights to nuclear power plant controllers. These processors help run factories, manage weapons systems, and enable the worldwide flow of information, products, and people. Unlike other computer systems such as those that operate personal computers, embedded systems must typically run error-free for years or even decades with little or no opportunity to reboot the system or fix problems. In addition, they require high performance, low cost, and low power consumption. Such systems typically consist of a heterogeneous collection of processors, specialized memory subsystems, and partially programmable or fixed-function components. This heterogeneity, coupled with issues such as hardware/software partitioning, mapping, and scheduling, leads to a large number of design possibilities, making performance debugging and validation of such systems a difficult problem and an imperative issue.

Roychoudhury guides readers through a host of debugging and verification methods critical to providing reliable software and systems applications. All the major abstraction levels of embedded systems design are covered. Readers will find practical information including:

Complete coverage of the major abstraction levels, from software analysis and microarchitectural modeling to modeling of resource sharing and communication at the system level.

Integration of formal validation techniques for hardware/software with debugging and validation of embedded system design flows.

Real-world case studies-to answer the questions: Does a design meet its requirements? If not, then which parts of the system are responsible for the violation? Once these are identified, then how should the design be suitably modified?

Contents:

Chapter 1 Introduction 1

Chapter 2 Model Validation 7

2.1 Platform versus System Behavior 8

2.2 Criteria for Design Model 10

2.3 Informal Requirements: A Case Study 12

2.3.1 The Requirements Document 13

2.3.2 Simplification of the Informal Requirements 14

2.4 Common Modeling Notations 16

2.4.1 Finite-State Machines 16

2.4.2 Communicating FSMs 20

2.4.3 Message Sequence Chart-Based Models 27

2.5 Remarks about Modeling Notations 37

2.6 Model Simulations 39

2.6.1 FSM Simulations 41

2.6.2 Simulating MSC-Based System Models 46

2.7 Model-Based Testing 50

2.8 Model Checking 58

2.8.1 Property Specification 58

2.8.2 Checking Procedure 73

2.9 The SPIN Validation Tool 82

2.10 The SMV Validation Tool 86

2.11 Case Study: Air-Traffic Controller 89

2.12 References 91

2.13 Exercises 93

Chapter 3 Communication Validation 95

3.1 Common Incompatibilities 98

3.1.1 Sending/Receiving Signals in Different Order 99

3.1.2 Handling a Different Signal Alphabet 100

3.1.3 Mismatch in Data Format 102

3.1.4 Mismatch in Data Rates 105

3.2 Converter Synthesis 106

3.2.1 Representing Native Protocols and Converters 106

3.2.2 Basic Ideas for Converter Synthesis 108

3.2.3 Various Strategies for Protocol Conversion 115

3.2.4 Avoiding No-Progress Cycles 116

3.2.5 Speculative Transmission to Avoid Deadlocks 118

3.3 Changing a Working Design 121

3.4 References 122

3.5 Exercises 123

Chapter 4 Performance Validation 125

4.1 The Conventional Abstraction of Time 126

4.2 Predicting Execution Time of a Program 131

4.2.1 WCET Calculation 133

4.2.2 Modeling of Microarchitecture 145

4.3 Interference with in a Processing Element 154

4.3.1 Interrupts from Environment 155

4.3.2 Contention and Preemption 157

4.3.3 Sharing a Processor Cache 161

4.4 System-Level Communication Analysis 165

4.5 Designing Systems with Predictable Timing 169

4.5.1 Scratchpad Memories 169

4.5.2 Time-Triggered Communication 174

4.6 Emerging Applications 176

4.7 References 177

4.8 Exercises 177

Chapter 5 Functionality Validation 181

5.1 Dynamic or Trace-Based Checking 184

5.1.1 Dynamic Slicing 187

5.1.2 Fault Localization 196

5.1.3 Directed Testing Methods 203

5.2 Formal Verification 207

5.2.1 Predicate Abstraction 211

5.2.2 Software Checking via Predicate Abstraction 218

5.2.3 Combining Formal Verification with Testing 225

5.3 References 229

5.4 Exercises 230.

Notes:

Includes bibliographical references (pages 233-239) and index.

Local Notes:

Acquired for the Penn Libraries with assistance from the Anne and Joseph Trachtman Memorial Book Fund.

ISBN:

9780123742308

0123742307

OCLC:

299711039

Publisher Number:

99935533151