嵌入式實時系統(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  自動機(jī)和語言
    2.2.1  語言和表示
    2.2.2   有限自動機(jī)
    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的擴(kuò)展
  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章  利用飾件自動機(jī)進(jìn)行驗證
第8章  時間相關(guān)的Petri網(wǎng)
第9章  進(jìn)程代數(shù)
第10章  基于命題邏輯規(guī)則系統(tǒng)的設(shè)計與分析
第11章  基于謂詞邏輯規(guī)則系統(tǒng)的時序分析
第12章  基于規(guī)則系統(tǒng)的優(yōu)化
參考文獻(xiàn)