Embedded Systems and Software Validation
- 1st Edition - May 29, 2009
- Latest edition
- Author: Abhik Roychoudhury
- Language: English
Modern embedded systems require high performance, low cost and low power consumption. Such systems typically consist of a heterogeneous collection of processors, specialized me… Read more
Modern embedded systems 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, scheduling, etc., leads to a large number of design possibilities, making performance debugging and validation of such systems a difficult problem.
Embedded systems are used to control safety critical applications such as flight control, automotive electronics and healthcare monitoring. Clearly, developing reliable software/systems for such applications is of utmost importance. This book describes a host of debugging and verification methods which can help to achieve this goal.
- Covers the major abstraction levels of embedded systems design, starting from software analysis and micro-architectural modeling, to modeling of resource sharing and communication at the system level
- Integrates formal techniques of validation for hardware/software with debugging and validation of embedded system design flows
- Includes practical 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, and once they are identified, then how should the design be suitably modified?
Designers of Microprocessors and Systems-on-Chip (SOC), concerned with debugging and validation, at companies globally such as Microsoft, Honeywell, Intel, and many more
1 Introduction
2 Model Validation 2.1 Platform vs System Behavior 2.2 Criteria for Design Model2.3 Informal Requirements: A Case Study 2.3.1 The Requirements Document2.3.2 Simplication of the Informal Requirements2.4 Common Modeling Notations2.4.1 Finite State Machines (FSM)2.4.2 Communicating FSMs2.4.3 Message Sequence Chart based Models 2.5 Remarks about Modeling Notations2.6 Model Simulations2.6.1 FSM simulations2.6.2 Simulating MSC-based System Models2.7 Model-based Testing2.8 Model Checking2.8.1 Property Specifcation2.8.2 Checking procedure2.9 The SPIN Validation Tool2.10 The SMV Validation Tool2.11 Case Study: Air Traffic Controller2.12 References2.13 Exercises
3 Communication Validation3.1 Common Incompatibilities 3.1.1 Sending/receiving signals in di erent order3.1.2 Handling a diffrent signal alphabet3.1.3 Mismatch in data format3.1.4 Mismatch in data rates3.2 Converter Synthesis 3.2.1 Representing Native Protocols and Converters3.2.2 Basic ideas for Converter synthesis3.2.3 Various strategies for protocol conversion3.2.4 Avoiding no-progress cycles3.2.5 Speculative transmission to avoid deadlocks3.3 Changing a working design 3.4 References3.5 Exercises
4 Performance Validation4.1 The Conventional Abstraction of Time4.2 Predicting Execution Time of a Program4.2.1 WCET Calculation 4.2.2 Modeling of Micro-architecture4.3 Interference within a Processing Element4.3.1 Interrupts from Environment4.3.2 Contention and Preemption4.3.3 Sharing a Processor Cache4.4 System level communication analysis4.5 Designing Systems with Predictable Timing4.5.1 Scratchpad Memories4.5.2 Time-triggered Communication4.6 Emerging applications4.7 References4.8 Exercises
5 Functionality Validation5.1 Dynamic or Trace-based Checking5.1.1 Dynamic Slicing5.1.2 Fault Localization5.1.3 Directed Testing Methods5.2 Formal Verifcation5.2.1 Predicate Abstraction5.2.2 Software Checking via Predicate Abstraction5.2.3 Combining Formal Verifcation with Testing5.3 References5.4 Exercises
- Edition: 1
- Latest edition
- Published: May 29, 2009
- Language: English
AR
Abhik Roychoudhury
Abhik received his M.S. and Ph.D. in Computer Science from the State University of New York at Stony Brook in 1997 and 2000 respectively. His research has focused on formal verification and analysis methods for system design, with focus on embedded software and systems. In these areas, his research group has been involved in building practical program analysis and software productivity tools which enhance software quality as well as programmer productivity. Two meaningful examples of such endeavor are the JSlice dynamic analysis tool for Java program debugging, and the Chronos static analysis tool for ensuring time-predictable execution of embedded software. His awards include a 2008 IBM Faculty Award. Since 2001, Abhik has been at the School of Computing in the National University of Singapore, where he is currently an Associate Professor.
Affiliations and expertise
Associate Professor, National University of Singapore