第1章 嵌入式軟件可信性保障技術(shù)體系
1．1 航天嵌入式控制系統(tǒng)的組成和特點
1．2 航天嵌入式控制軟件中的可信問題
1．2．1 實時性問題
1．2．2 內(nèi)存使用問題
1．2．3 數(shù)據(jù)使用問題
1．2．4 計算問題
1．2．5 協(xié)議正確性問題
1．2．6 狀態(tài)轉(zhuǎn)換問題
1．2．7 故障處理問題
1．2．8 編譯等價性問題
1．2．9 編碼問題
1．2．10 各階段一致性問題
1．3 可信保障五維體系結(jié)構(gòu)模型
1．4 實例：時序保障問題分析
1．4．1 需求分析階段的保障
1．4．2 設(shè)計階段的保障
1．4．3 編碼階段的保障
1．4．4 測試階段的保障
1．4．5 方法、技術(shù)和工具
1．4．6 度量

第2章 航天控制軟件需求建模與驗證
2．1 需求建模語言
2．1．1 建模語法定義
2．1．2 建模語義解釋
2．2 需求性質(zhì)描述語言
2．2．1 性質(zhì)描述語法定義
2．2．2 性質(zhì)描述語義解釋
2．2．3 性質(zhì)描述模板
2．3 分析與驗證方法
2．3．1 類型檢查
2．3．2 數(shù)據(jù)流分析
2．3．3 原型生成與快速仿真
2．3．4 隨機語義
2．3．5 概率模型檢查
2．4 SPRADL應(yīng)用框架

第3章 程序?qū)崿F(xiàn)正確性保障
3．1 可信編程規(guī)范
3．1．1 禁止使用的C語言特性
3．1．2 語言使用規(guī)則
3．1．3 領(lǐng)域相關(guān)規(guī)則
3．1．4 環(huán)境相關(guān)規(guī)則
3．1．5 檢測工具介紹
3．2 數(shù)值性質(zhì)分析技術(shù)
3．2．1 基于抽象解釋的數(shù)值性質(zhì)分析技術(shù)
3．2．2 區(qū)間抽象域的基本定義及操作
3．2．3 區(qū)間抽象域的冪集拓展
3．2．4 基于浮點區(qū)間冪集的程序分析方法
3．3 數(shù)據(jù)競爭預(yù)防和檢測技術(shù)
3．3．1 典型數(shù)據(jù)競爭案例及分析
3．3．2 避免數(shù)據(jù)競爭的設(shè)計策略
3．3．3 數(shù)據(jù)競爭檢測方法及工具
3．4 單元測試用例自動生成技術(shù)
3．4．1 測試技術(shù)
3．4．2 應(yīng)用實例
3．5 數(shù)字虛擬仿真測試技術(shù)
3．5．1 數(shù)字虛擬仿真測試平臺的功能
3．5．2 數(shù)字虛擬仿真測試平臺構(gòu)建技術(shù)
3．5．3 數(shù)字虛擬仿真測試平臺

第4章 嵌入式軟件形式化驗證
4．1 模型檢驗
4．1．1 軟件模型檢驗技術(shù)
4．1．2 嵌入式軟件模型檢驗技術(shù)
4．1．3 模型檢驗工具
4．1．4 面向源程序的模型檢驗應(yīng)用舉例
4．2 定理證明
4．2．1 定理證明技術(shù)
4．2．2 嵌入式操作系統(tǒng)的形式化驗證舉例

第5章 嵌入式軟件可信保障集成環(huán)境
5．1 集成環(huán)境的需求和功能
5．2 集成環(huán)境的集成方法
5．2．1 集成對象
5．2．2 集成方法
5．3 集成環(huán)境實現(xiàn)
5．3．1 集成環(huán)境體系架構(gòu)
5．3．2 集成環(huán)境的實現(xiàn)技術(shù)
5．3．3 設(shè)計實現(xiàn)
5．3．4 工具集成與應(yīng)用舉例
縮略語
參考文獻