圖書信息
作 者：（印）羅伊喬杜里 著，田尊華 譯
嵌入式系統設計的驗證與調試技術
出 版 社：清華大學出版社
出版時間：2010-7-1
版 次：1
頁 數：200
字 數：278000
印刷時間：2010-7-1
開 本：16開
紙 張：膠版紙
印 次：1
I S B N：9787302230724
包 裝：平裝
內容簡介
《嵌入式系統設計的驗證與調試技術》系統介紹了適用於嵌入式系統設計整個生命周期的實用調試和驗證技術，涵蓋了嵌入式系統設計和各個主要的抽象層次。在掌握了本書介紹的大量的高度和驗證技術後，讀者可以構建出可靠的嵌入式系統和軟體。
全書結構合理清晰，內容全面豐富，適合所有從事嵌入式研究與開發的專業人員閱讀，同時對於模型驗證方面的研究人員也具有重要的參考價值。
作者簡介
羅伊喬杜里博士是新加坡國立大學的副教授，從紐約州立大學石溪分校獲得了計算機科學的博士學位。他的研究方向為嵌入式軟體和系統的建模與驗證。Abhik發表了超過60篇論文及著作。他的研究成功地實現了針對嵌入式軟體的可擴展的實用分析工具，用於提高軟體的質量和程式設計師的效率。Abhik是軟體工程和嵌入式系統方面許多大中型基金項目的首席研究員。他獲得過多種獎項，包括IBM優秀員工獎和陳嘉庚青少年發明家獎。
目錄
第1章 嵌入式系統驗證簡介/1
第2章 模型驗證/5
2.1 平台與系統行為/6
2.2 模型設計準則/8
2.3 非形式化需求：案例分析/9
2.3.1 需求文檔/10
2.3.2 非形式化需求簡化/11
2.4 通用建模概念/13
2.4.1 有限狀態機/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的系統模型仿真/39
2.7 基於模型的測試/43
2.8 模型校驗/50
2.8.1 屬性規範/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 以不同的順序傳送/接收信號/86
3.1.2 處理不同的信號字母表/87
3.1.3 數據格式不匹配/89
3.1.4 數據率不匹配/91
3.2 轉換器合成/92
3.2.1 本地協定和轉換器的表示/92
3.2.2 轉換器合成的基本思想/94
3.2.3 各種協定轉換策略/100
3.2.4 避免不推進循環/101
3.2.5 避免死鎖的投機傳輸/102
3.3 改變工作設計/105
3.4 參考文獻/106
3.5 習題/107
第4章 性能驗證/109
4.1 傳統時間抽象/110
4.2 預測程式執行時間/114
4.2.1WCET計算/116
4.2.2微體系結構建模/127
4.3 處理單元內部的干擾/135
4.3.1 來自環境的中斷/135
4.3.2 競爭與搶占/137
4.3.3 共享處理器快取/141
4.4 系統級通信分析/144
4.5 設計可預測時間的系統/147
4.5.1 中間結果存儲器/147
4.5.2 時間觸發通信/152
4.6 新興套用/154
4.7 參考文獻/154
4.8 習題/155
第5章功能驗證/157
5.1 動態或基於軌跡的校驗/159
5.1.1 動態切片/163
5.1.2 錯誤定位/171
5.1.3 導引測試方法/177
5.2 形式化校核/180
5.2.1 謂詞抽象/183
5.2.2 通過謂詞抽象進行軟體校驗/189
5.2.3 形式化校核與測試的結合/195
5.3 參考文獻/198
5.4 習題/199
