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

定　價：￥29.00

作　者：	（印）羅伊喬杜里著，田尊華譯
出版社：	清華大學出版社
叢編項：	國外計算機科學經(jīng)典教材
標　簽：	計算機理論

購買這本書可以去

ISBN：	9787302230724	出版時間：	2010-07-01	包裝：	平裝
開本：	16開	頁數(shù)：	200	字數(shù)：

內(nèi)容簡介

　　《嵌入式系統(tǒng)設(shè)計的驗證與調(diào)試技術(shù)》系統(tǒng)介紹了適用于嵌入式系統(tǒng)設(shè)計整個生命周期的實用調(diào)試和驗證技術(shù)，涵蓋了嵌入式系統(tǒng)設(shè)計的各個主要的抽象層次。在掌握了《嵌入式系統(tǒng)設(shè)計的驗證與調(diào)試技術(shù)》介紹的大量的調(diào)試和驗證技術(shù)后，讀者可以構(gòu)建出可靠的嵌入式系統(tǒng)和軟件。全書結(jié)構(gòu)合理清晰，內(nèi)容全面豐富，適合所有從事嵌入式研究與開發(fā)的專業(yè)人員閱讀，同時對于模型驗證方面的研究人員也具有重要的參考價值。

作者簡介

　　羅伊喬杜里（Abhik Roychoudhury），博士是新加坡國立大學的副教授，從紐約州立大學石溪分校獲得了計算機科學的博士學位。他的研究方向為嵌入式軟件和系統(tǒng)的建模與驗證。Abhik發(fā)表了超過60篇論文及著作。他的研究成功地實現(xiàn)了針對嵌入式軟件的可擴展的實用分析工具，用于提高軟件的質(zhì)量和程序員的效率。Abhik是軟件工程和嵌入式系統(tǒng)方面許多大中型基金項目的首席研究員。他獲得過多種獎項，包括IBM優(yōu)秀員工獎和陳嘉庚青少年發(fā)明家獎。

圖書目錄

第1章嵌入式系統(tǒng)驗證簡介/1
第2章模型驗證/5
2.1 平臺與系統(tǒng)行為/6
2.2 模型設(shè)計準則/8
2.3 非形式化需求：案例分析/9
2.3.1 需求文檔/10
2.3.2 非形式化需求簡化/11
2.4 通用建模概念/13
2.4.1 有限狀態(tài)機/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 基于模型的測試/43
2.8 模型校驗/50
2.8.1 屬性規(guī)范/50
2.8.2 校驗過程/63
2.9 SPIN驗證工具/71
2.10 SMV驗證工具/74
2.11 案例分析：空中交通管制器/77
2.12 參考文獻/79
2.13 習題/80
第3章通信驗證/83
3.1 常見不兼容性/86
3.1.1 以不同的順序發(fā)送/接收信號/86
3.1.2 處理不同的信號字母表/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 避免不推進循環(huán)/101
3.2.5 避免死鎖的投機傳輸/102
3.3 改變工作設(shè)計/105
3.4 參考文獻/106
3.5 習題/107
第4章性能驗證/109
4.1 傳統(tǒng)時間抽象/110
4.2 預測程序執(zhí)行時間/114
4.2.1 WCET計算/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)級通信分析/144
4.5 設(shè)計可預測時間的系統(tǒng)/147
4.5.1 中間結(jié)果存儲器/147
4.5.2 時間觸發(fā)通信/152
4.6 新興應用/154
4.7 參考文獻/154
4.8 習題/155
第5章功能驗證/157
5.1 動態(tài)或基于軌跡的校驗/159
5.1.1 動態(tài)切片/163
5.1.2 錯誤定位/171
5.1.3 導引測試方法/177
5.2 形式化校核/180
5.2.1 謂詞抽象/183
5.2.2 通過謂詞抽象進行軟件校驗/189
5.2.3 形式化校核與測試的結(jié)合/195
5.3 參考文獻/198
5.4 習題/199