嵌入式實時系統(tǒng)

定　價：￥69.00

作　者：	（美）阿爾伯特陳著，周強，李峭，楊昕欣譯
出版社：	北京航空航天大學(xué)出版社
叢編項：	調(diào)度、分析和驗證
標(biāo)　簽：	計算機考試考試軟件水平考試

購買這本書可以去

當(dāng)當(dāng)網(wǎng)

ISBN：	9787512418714	出版時間：	2015-12-01	包裝：	平裝
開本：	16開	頁數(shù)：	403	字數(shù)：

內(nèi)容簡介

　　阿爾伯特陳*作的《嵌入式實時系統(tǒng)：調(diào)度分析和驗證/嵌入式系統(tǒng)譯叢》面向嵌入式實時系統(tǒng)，較系統(tǒng)地論述基本的實時調(diào)度算法、調(diào)度性分析方法，說明引入形式化方法的必要性，并為實時系統(tǒng)設(shè)計提供一個清晰的形式化方法基礎(chǔ)。其核心是面向?qū)崟r系統(tǒng)的形式化分析（forreal analysis）及驗證。全書特別列舉了大量關(guān)于安全關(guān)鍵系統(tǒng)的工程實例，從簡單系統(tǒng)（如溫度控制系統(tǒng)、面包機和電飯煲）到高度復(fù)雜系統(tǒng)（如飛機和航天飛機），通過將上述形式化方法成功應(yīng)用于這些工程項目，有助于加深讀者對嵌入式實時系統(tǒng)分析和驗證方法的理解和運用。本書面向高等院校本科生和研究生，作為“嵌入式系統(tǒng)”、“實時系統(tǒng)”相關(guān)專業(yè)課程教材或教學(xué)參考書使用；也可面向業(yè)界從業(yè)者和研究人員，作為參考書使用。

作者簡介

暫缺《嵌入式實時系統(tǒng)》作者簡介

圖書目錄

第1章簡介
1.1 什么是時間
1.2 仿真
1.3 測試
1.4 驗證
1.5 運行時期監(jiān)測
1.6 相關(guān)資源
第2章非實時系統(tǒng)的分析與驗證
2.1 符號邏輯
    2.1.1 命題邏輯
    2.1.2 謂詞邏輯
2.2 自動機和語言
    2.2.1 語言和表示
    2.2.2   有限自動機
    2.2.3 非定時系統(tǒng)的規(guī)范指定和驗證
2.3 歷史回顧和相關(guān)研究
2.4 總結(jié)
習(xí)題
第3章實時調(diào)度和調(diào)度性分析
3.1 確定計算時間
3.2 單處理器調(diào)度
    3.2.1 獨立可搶占任務(wù)的調(diào)度
    3.2.2 不可搶占任務(wù)的調(diào)度
    3.2.3 帶前后次序約束的不可搶占任務(wù)
    3.2.4 周期任務(wù)間的通信：確定的會合模型
    3.2.5 帶臨界區(qū)域的周期任務(wù)：核心化監(jiān)測模型
3.3 多處理器調(diào)度
    3.3.1 調(diào)度表示
    3.3.2 單實例任務(wù)調(diào)度
    3.3.3 周期任務(wù)調(diào)度
3.4 可用的調(diào)度工具
    3.4.1 PERTS/RAPID RMA
    3.4.2 PerfoRMAx
    3.4.3 TimeWiz
3.5 可用的實時操作系統(tǒng)
3.6 歷史回顧和相關(guān)研究
3.7 總結(jié)
習(xí)題
第4章有限狀態(tài)系統(tǒng)的模型檢測
4.1 系統(tǒng)規(guī)范
4.2 CLARKE-EMERSON-SISTLA模型檢測器
4.3 CTL的擴展
4.4 應(yīng)用
4.5 用C實現(xiàn)的完整的CTL模型檢測器程序
4.6 符號化模型檢測
    4.6.1 二元決策圖BDDs
    4.6.2 符號模型檢測器
4.7 實時CTL
    4.7.1 最小和最大延遲
    4.7.2 條件發(fā)生的最小和最大數(shù)量
    4.7.3 非單位轉(zhuǎn)移時間
4.8 可用的工具
4.9 歷史回顧和相關(guān)研究
4.10 總結(jié)
習(xí)題
第5章可視形式化、狀態(tài)圖和STATEMATE
5.1 狀態(tài)圖
    5.1.1 狀態(tài)圖的基本功能
    5.1.2 語義
5.2 活動圖
……
第6章實時邏輯、圖論分析與模式圖
第7章利用飾件自動機進行驗證
第8章時間相關(guān)的Petri網(wǎng)
第9章進程代數(shù)
第10章基于命題邏輯規(guī)則系統(tǒng)的設(shè)計與分析
第11章基于謂詞邏輯規(guī)則系統(tǒng)的時序分析
第12章基于規(guī)則系統(tǒng)的優(yōu)化
參考文獻