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

定　價(jià)：￥69.00

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

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

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

ISBN：	9787512418714	出版時(shí)間：	2015-12-01	包裝：	平裝
開(kāi)本：	16開(kāi)	頁(yè)數(shù)：	403	字?jǐn)?shù)：

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

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

作者簡(jiǎn)介

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

圖書(shū)目錄

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