嵌入式系統(tǒng)設(shè)計(jì)的驗(yàn)證與調(diào)試技術(shù)

第1章 嵌入式系統(tǒng)驗(yàn)證簡介/1
第2章 模型驗(yàn)證/5
2.1 平臺(tái)與系統(tǒng)行為/6
2.2 模型設(shè)計(jì)準(zhǔn)則/8
2.3 非形式化需求：案例分析/9
2.3.1 需求文檔/10
2.3.2 非形式化需求簡化/11
2.4 通用建模概念/13
2.4.1 有限狀態(tài)機(jī)/13
2.4.2 FSM通信/16
2.4.3 基于消息順序圖的模型/22
2.5 建模概念討論/31
2.6 模型仿真/33
2.6.1 FSM仿真/35
2.6.2 基于MSC的系統(tǒng)模型仿真/39
2.7 基于模型的測(cè)試/43
2.8 模型校驗(yàn)/50
2.8.1 屬性規(guī)范/50
2.8.2 校驗(yàn)過程/63
2.9 SPIN驗(yàn)證工具/71
2.10 SMV驗(yàn)證工具/74
2.11 案例分析：空中交通管制器/77
2.12 參考文獻(xiàn)/79
2.13 習(xí)題/80
第3章 通信驗(yàn)證/83
3.1 常見不兼容性/86
3.1.1 以不同的順序發(fā)送/接收信號(hào)/86
3.1.2 處理不同的信號(hào)字母表/87
3.1.3 數(shù)據(jù)格式不匹配/89
3.1.4 數(shù)據(jù)率不匹配/91
3.2 轉(zhuǎn)換器合成/92
3.2.1 本地協(xié)議和轉(zhuǎn)換器的表示/92
3.2.2 轉(zhuǎn)換器合成的基本思想/94
3.2.3 各種協(xié)議轉(zhuǎn)換策略/100
3.2.4 避免不推進(jìn)循環(huán)/101
3.2.5 避免死鎖的投機(jī)傳輸/102
3.3 改變工作設(shè)計(jì)/105
3.4 參考文獻(xiàn)/106
3.5 習(xí)題/107
第4章 性能驗(yàn)證/109
4.1 傳統(tǒng)時(shí)間抽象/110
4.2 預(yù)測(cè)程序執(zhí)行時(shí)間/114
4.2.1 WCET計(jì)算/116
4.2.2 微體系結(jié)構(gòu)建模/127
4.3 處理單元內(nèi)部的干擾/135
4.3.1 來自環(huán)境的中斷/135
4.3.2 競爭與搶占/137
4.3.3 共享處理器緩存/141
4.4 系統(tǒng)級(jí)通信分析/144
4.5 設(shè)計(jì)可預(yù)測(cè)時(shí)間的系統(tǒng)/147
4.5.1 中間結(jié)果存儲(chǔ)器/147
4.5.2 時(shí)間觸發(fā)通信/152
4.6 新興應(yīng)用/154
4.7 參考文獻(xiàn)/154
4.8 習(xí)題/155
第5章 功能驗(yàn)證/157
5.1 動(dòng)態(tài)或基于軌跡的校驗(yàn)/159
5.1.1 動(dòng)態(tài)切片/163
5.1.2 錯(cuò)誤定位/171
5.1.3 導(dǎo)引測(cè)試方法/177
5.2 形式化校核/180
5.2.1 謂詞抽象/183
5.2.2 通過謂詞抽象進(jìn)行軟件校驗(yàn)/189
5.2.3 形式化校核與測(cè)試的結(jié)合/195
5.3 參考文獻(xiàn)/198
5.4 習(xí)題/199