嵌入式系統(tǒng)設計的驗證與調試技術

前言

　　21世紀是信息時代，尤其是計算機時代，也可以講21世紀是嵌入式系統(tǒng)時代。從復雜的航天系統(tǒng)到簡單的遙控器，無不與嵌入式系統(tǒng)相關。嵌入式系統(tǒng)已經與我們的日常生活密切相關，例如，移動電話、PDA、電子閱讀器、各種家電、汽車、門禁系統(tǒng)、各種IC卡等等，可以講，如果現(xiàn)在離開了嵌入式系統(tǒng)，我們的日常生活工作將無法正常進行。嵌入式計算就是在這種背景下提出來的，這也足以說明嵌入式系統(tǒng)的普及程度和重要性?！　陌踩煽康慕嵌葋碇v，嵌入式系統(tǒng)可以分為安全關鍵的(safety-critical)和非(或一般)安全關鍵的。屬于安全關鍵的嵌入式系統(tǒng)有車輛、飛行、核電廠和醫(yī)療設備等方面的控制系統(tǒng)。屬于非(或一般)安全關鍵的嵌入式系統(tǒng)有移動電話、HDTV、家電控制器等。不管嵌入式系統(tǒng)是否為安全關鍵的，可靠性都很重要。安全關鍵的系統(tǒng)出現(xiàn)問題可能意味著巨大的生命財產損失，而對于非(或一般)安全關鍵的嵌入式系統(tǒng)來說，出現(xiàn)問題時即便不會造成任何生命財產損失，也意味著對用戶使用信心的打擊，而這將直接關系到相關產品的市場前景。那么如何保證嵌入式系統(tǒng)和軟件的可靠性呢?本書正是為此而編寫。本書系統(tǒng)地講述了嵌入式系統(tǒng)設計流程中各個階段的驗證問題。當然，根據(jù)嵌入式系統(tǒng)不同的安全需求，考慮到成本因素，在驗證上可以區(qū)分對待。相比一般系統(tǒng)而言，對于安全關鍵的系統(tǒng)必須進行更加嚴格的驗證。　　本書的顯著特征是針對嵌入式系統(tǒng)和軟件這個特定的領域，從不同的層面系統(tǒng)地討論了各種驗證方法。本書具有的第二個特點是，與一般講理論的書不同，本書在講述過程中緊密結合具體示例(如空中交通管制系統(tǒng)和汽車控制系統(tǒng))和標準案例(西門子基準測試套件中的代碼段)。此外，本書還有針對性地給出了少而精的習題，為鞏固相關知識和激發(fā)讀者思考提供了良好的題材?！　”緯蓢揽茖W技術大學的田尊華翻譯，由肖國尊負責監(jiān)督本書的翻譯質量和進度。鑒于譯者水平有限，時間倉促，不足和疏漏之處在所難免，敬請廣大讀者提供反饋意見。

內容概要

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

作者簡介

羅伊喬杜里博士是新加坡國立大學的副教授，從紐約州立大學石溪分校獲得了計算機科學的博士學位。他的研究方向為嵌入式軟件和系統(tǒng)的建模與驗證。Abhik發(fā)表了超過60篇論文及著作。他的研究成功地實現(xiàn)了針對嵌入式軟件的可擴展的實用分析工具，用于提高軟件的質量和程序員的

書籍目錄

第1章  嵌入式系統(tǒng)驗證簡介/1第2章  模型驗證/5  2.1  平臺與系統(tǒng)行為/6  2.2  模型設計準則/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  轉換器合成/92    3.2.1  本地協(xié)議和轉換器的表示/92    3.2.2  轉換器合成的基本思想/94    3.2.3  各種協(xié)議轉換策略/100    3.2.4  避免不推進循環(huán)/101    3.2.5  避免死鎖的投機傳輸/102  3.3  改變工作設計/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  微體系結構建模/127  4.3  處理單元內部的干擾/135    4.3.1  來自環(huán)境的中斷/135    4.3.2  競爭與搶占/137    4.3.3  共享處理器緩存/141  4.4  系統(tǒng)級通信分析/144  4.5  設計可預測時間的系統(tǒng)/147    4.5.1  中間結果存儲器/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  形式化校核與測試的結合/195  5.3  參考文獻/198  5.4  習題/199

章節(jié)摘錄

　?。?）當A1℃的狀態(tài)為預更新時，它會發(fā)送消息，引導所有連接的客戶端獲取新的天氣信息，然后將自己的狀態(tài)和客戶端的狀態(tài)都設置為更新（updating）。　　（4）如果所有客戶端報告成功獲取新天氣信息，那么ATC會發(fā)送消息通知這些客戶端使用新的天氣信息，然后將自己的狀態(tài)和這些客戶端的狀態(tài)都設置為后更新（postupdating）。　　否則，如果任何連接的客戶端報告獲取新天氣信息失敗，那么ATC會發(fā)送消息給所有的客戶端，告訴它們使用自己原來的天氣信息，然后將自己的狀態(tài)和這些客戶端的狀態(tài)都設置為后恢復（postreverting）?！　。?）當ATC的狀態(tài)為后更新時，如果所有這些客戶端都報告成功使用了新天氣信息，那么更新就完成了。ATC會將自己的狀態(tài)和這些客戶端的狀態(tài)設置為空閑，并重新將WCP設為啟用?！　》駝t，如果任何連接的客戶端報告使用新天氣信息失敗，那么ATC會斷開所有連接的客戶端，重新將WCP設置為啟用，并將自己的狀態(tài)重新設置為空閑。　?。?）當ATC的狀態(tài)為后恢復時，如果所有的客戶端都報告使用原天氣信息成功，那么恢復過程就完成了。ATC會將自己的狀態(tài)和這些客戶端的狀態(tài)都設置為空閑，并將WCP設為啟用?！　》駝t，如果任何連接的客戶端報告使用原天氣信息失敗，那么.ATC會斷開所有連接的客戶端，重新將WCP設置為啟用，并將自己的狀態(tài)重新設置為空閑?！　∽⑨尅　∏懊娴暮喕枨竽軌蜃屓烁杏X到現(xiàn)實系統(tǒng)的需求文檔，盡管這只是一個非常概略的需求。這個規(guī)范無疑是可以理解的，然而我們卻不能直接通過它找出其中的錯誤。實際上剛才給出的這個非形式化規(guī)范存在死鎖錯誤，即系統(tǒng)可能達到一個沒有動作可以執(zhí)行的狀態(tài)?，F(xiàn)在，我們繼續(xù)研究能夠檢測、甚至有助于改正這類錯誤的建模概念和校驗過程（基于這些建模概念）。

編輯推薦

　　《嵌入式系統(tǒng)設計的驗證與調試技術》特色：　　《嵌入式系統(tǒng)設計的驗證與調試技術》嵌入式系統(tǒng)軟件驗證方面的先驅之作。　　針對嵌入式系統(tǒng)和軟件這個特定的領域，從不同的層面系統(tǒng)地討論了各種驗證方法?！　【o密結合具體示例和標準案例，并有針對性地給出了少而精的習題，為鞏固相關知識和激發(fā)讀者思考提供了良好的題材。

圖書封面

圖書標簽Tags

無

評論、評分、閱讀與下載

---

    嵌入式系統(tǒng)設計的驗證與調試技術 PDF格式下載

---