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

定　價(jià)：￥29.00

作　者：	（?。┝_伊喬杜里著，田尊華譯
出版社：	清華大學(xué)出版社
叢編項(xiàng)：	國(guó)外計(jì)算機(jī)科學(xué)經(jīng)典教材
標(biāo)　簽：	計(jì)算機(jī)理論

購(gòu)買(mǎi)這本書(shū)可以去

ISBN：	9787302230724	出版時(shí)間：	2010-07-01	包裝：	平裝
開(kāi)本：	16開(kāi)	頁(yè)數(shù)：	200	字?jǐn)?shù)：

內(nèi)容簡(jiǎn)介

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

作者簡(jiǎn)介

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

圖書(shū)目錄

第1章嵌入式系統(tǒng)驗(yàn)證簡(jiǎ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 非形式化需求簡(jiǎn)化/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)過(guò)程/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 常見(jiàn)不兼容性/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 來(lái)自環(huán)境的中斷/135
4.3.2 競(jìng)爭(zhēng)與搶占/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 通過(guò)謂詞抽象進(jìn)行軟件校驗(yàn)/189
5.2.3 形式化校核與測(cè)試的結(jié)合/195
5.3 參考文獻(xiàn)/198
5.4 習(xí)題/199