Embedded Systems and Software Validation (Hardcover)

<內容簡介>

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.
 <章節目錄>

1 Introduction

2 Model Validation

2.1 Platform vs System Behavior
2.2 Criteria for Design Model
2.3 Informal Requirements: A Case Study
2.3.1 The Requirements Document
2.3.2 Simplication of the Informal Requirements
2.4 Common Modeling Notations
2.4.1 Finite State Machines (FSM)
2.4.2 Communicating FSMs
2.4.3 Message Sequence Chart based Models
2.5 Remarks about Modeling Notations
2.6 Model Simulations
2.6.1 FSM simulations
2.6.2 Simulating MSC-based System Models
2.7 Model-based Testing
2.8 Model Checking
2.8.1 Property Specifcation
2.8.2 Checking procedure
2.9 The SPIN Validation Tool
2.10 The SMV Validation Tool
2.11 Case Study: Air Traffic Controller
2.12 References
2.13 Exercises

3 Communication Validation

3.1 Common Incompatibilities
3.1.1 Sending/receiving signals in di erent order
3.1.2 Handling a diffrent signal alphabet
3.1.3 Mismatch in data format
3.1.4 Mismatch in data rates
3.2 Converter Synthesis
3.2.1 Representing Native Protocols and Converters
3.2.2 Basic ideas for Converter synthesis
3.2.3 Various strategies for protocol conversion
3.2.4 Avoiding no-progress cycles
3.2.5 Speculative transmission to avoid deadlocks
3.3 Changing a working design
3.4 References
3.5 Exercises

4 Performance Validation

4.1 The Conventional Abstraction of Time
4.2 Predicting Execution Time of a Program
4.2.1 WCET Calculation
4.2.2 Modeling of Micro-architecture
4.3 Interference within a Processing Element
4.3.1 Interrupts from Environment
4.3.2 Contention and Preemption
4.3.3 Sharing a Processor Cache
4.4 System level communication analysis
4.5 Designing Systems with Predictable Timing
4.5.1 Scratchpad Memories
4.5.2 Time-triggered Communication
4.6 Emerging applications
4.7 References
4.8 Exercises

5 Functionality Validation

5.1 Dynamic or Trace-based Checking
5.1.1 Dynamic Slicing
5.1.2 Fault Localization
5.1.3 Directed Testing Methods
5.2 Formal Verifcation
5.2.1 Predicate Abstraction
5.2.2 Software Checking via Predicate Abstraction
5.2.3 Combining Formal Verifcation with Testing
5.3 References
5.4 Exercises

現代嵌入式系統需要高性能、低成本和低功耗。這些系統通常由異構的處理器集合、專用的記憶子系統和部分可編程或固定功能的組件組成。這種異構性，加上硬體/軟體分割、映射、調度等問題，導致設計可能性眾多，使得這類系統的性能調試和驗證成為一個困難的問題。

嵌入式系統用於控制飛行控制、汽車電子和醫療監測等安全關鍵應用。顯然，為這類應用開發可靠的軟體/系統至關重要。本書描述了一系列可以幫助實現此目標的調試和驗證方法。

1 簡介
2 模型驗證
2.1 平台與系統行為
2.2 設計模型的標準
2.3 非正式需求：案例研究
2.3.1 需求文件
2.3.2 簡化非正式需求
2.4 常見的建模符號
2.4.1 有限狀態機（FSM）
2.4.2 通信FSM
2.4.3 基於消息序列圖的模型
2.5 關於建模符號的備註
2.6 模型模擬
2.6.1 FSM模擬
2.6.2 模擬基於MSC的系統模型
2.7 基於模型的測試
2.8 模型檢查
2.8.1 屬性規範
2.8.2 檢查程序
2.9 SPIN驗證工具
2.10 SMV驗證工具
2.11 案例研究：空中交通管制
2.12 參考文獻
2.13 練習題

3 通信驗證
3.1 常見的不相容性
3.1.1 按不同順序發送/接收信號
3.1.2 處理不同的信號字母表
3.1.3 數據格式不匹配
3.1.4 數據速率不匹配
3.2 轉換器合成
3.2.1 表示本地協議和轉換器
3.2.2 轉換器合成的基本思想
3.2.3 協議轉換的各種策略
3.2.4 避免無進展的循環
3.2.5 通過推測傳輸避免死鎖
3.3 更改工作設計
3.4 參考文獻
3.5 練習題

4 性能驗證
4.1 傳統的時間抽象
4.2 預測程序的執行時間
4.2.1 WCET計算
4.2.2 微架構建模
4.3 處理元件內的干擾
4.3.1 環境中的中斷
4.3.2 競爭和抢占
4.3.3 共享處理器緩存
4.4 系統級通信分析
4.5 設計具有可預測時間的系統
4.5.1 Scratchpad記憶體
4.5.2 基於時間觸發的通信
4.6