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

第1章  簡介
  1.1  什么是時(shí)間
  1.2  仿真
  1.3  測試
  1.4  驗(yàn)證
  1.5  運(yùn)行時(shí)期監(jiān)測
  1.6  相關(guān)資源
第2章  非實(shí)時(shí)系統(tǒng)的分析與驗(yàn)證
  2.1  符號邏輯
    2.1.1  命題邏輯
    2.1.2  謂詞邏輯
  2.2  自動(dòng)機(jī)和語言
    2.2.1  語言和表示
    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ù)間的通信：確定的會合模型
    3.2.5  帶臨界區(qū)域的周期任務(wù)：核心化監(jiān)測模型
  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)的模型檢測
  4.1  系統(tǒng)規(guī)范
  4.2  CLARKE-EMERSON-SISTLA模型檢測器
  4.3  CTL的擴(kuò)展
  4.4  應(yīng)用
  4.5  用C實(shí)現(xiàn)的完整的CTL模型檢測器程序
  4.6 符號化模型檢測
    4.6.1  二元決策圖BDDs
    4.6.2  符號模型檢測器
  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  語義
  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)