可信的航天嵌入式控制軟件開(kāi)發(fā)技術(shù)
定 價(jià):62 元
叢書(shū)名:國(guó)防科技圖書(shū)出版基金
- 作者:楊孟飛,顧斌,郭向英 等 著
- 出版時(shí)間:2017/12/1
- ISBN:9787118112665
- 出 版 社:國(guó)防工業(yè)出版社
- 中圖法分類(lèi):V4-39
- 頁(yè)碼:176
- 紙張:膠版紙
- 版次:1
- 開(kāi)本:16開(kāi)
《可信的航天嵌入式控制軟件開(kāi)發(fā)技術(shù)》主要介紹航天嵌入式控制軟件可信保障技術(shù)體系及其關(guān)鍵技術(shù)。首先從近年來(lái)的實(shí)際案例提煉出影響航天嵌入式軟件可信性的十大可信問(wèn)題,針對(duì)這些關(guān)鍵可信問(wèn)題,從問(wèn)題、階段、方法、工具和度量五個(gè)維度進(jìn)行研究,形成了具有五維體系結(jié)構(gòu)的可信性保障技術(shù)體系;然后,重點(diǎn)論述了需求建模與驗(yàn)證、程序?qū)崿F(xiàn)正確性保障、嵌入式軟件形式化驗(yàn)證等關(guān)鍵問(wèn)題的解決方案;最后依據(jù)可信保障技術(shù)體系的需求,介紹了構(gòu)建嵌入式軟件可信保障集成環(huán)境的集成方法、體系架構(gòu)和關(guān)鍵技術(shù)。
《可信的航天嵌入式控制軟件開(kāi)發(fā)技術(shù)》針對(duì)嵌入式軟件研制中的實(shí)際問(wèn)題給出系統(tǒng)的解決方案,實(shí)用性強(qiáng),對(duì)于在航天行業(yè)以及航空、兵器、汽車(chē)、核電等行業(yè)從事嵌入式軟件研制的工程技術(shù)人員和系統(tǒng)總體設(shè)計(jì)人員,具有很好的參考價(jià)值。
第1章 嵌入式軟件可信性保障技術(shù)體系
1.1 航天嵌入式控制系統(tǒng)的組成和特點(diǎn)
1.2 航天嵌入式控制軟件中的可信問(wèn)題
1.2.1 實(shí)時(shí)性問(wèn)題
1.2.2 內(nèi)存使用問(wèn)題
1.2.3 數(shù)據(jù)使用問(wèn)題
1.2.4 計(jì)算問(wèn)題
1.2.5 協(xié)議正確性問(wèn)題
1.2.6 狀態(tài)轉(zhuǎn)換問(wèn)題
1.2.7 故障處理問(wèn)題
1.2.8 編譯等價(jià)性問(wèn)題
1.2.9 編碼問(wèn)題
1.2.10 各階段一致性問(wèn)題
1.3 可信保障五維體系結(jié)構(gòu)模型
1.4 實(shí)例:時(shí)序保障問(wèn)題分析
1.4.1 需求分析階段的保障
1.4.2 設(shè)計(jì)階段的保障
1.4.3 編碼階段的保障
1.4.4 測(cè)試階段的保障
1.4.5 方法、技術(shù)和工具
1.4.6 度量
第2章 航天控制軟件需求建模與驗(yàn)證
2.1 需求建模語(yǔ)言
2.1.1 建模語(yǔ)法定義
2.1.2 建模語(yǔ)義解釋
2.2 需求性質(zhì)描述語(yǔ)言
2.2.1 性質(zhì)描述語(yǔ)法定義
2.2.2 性質(zhì)描述語(yǔ)義解釋
2.2.3 性質(zhì)描述模板
2.3 分析與驗(yàn)證方法
2.3.1 類(lèi)型檢查
2.3.2 數(shù)據(jù)流分析
2.3.3 原型生成與快速仿真
2.3.4 隨機(jī)語(yǔ)義
2.3.5 概率模型檢查
2.4 SPRADL應(yīng)用框架
第3章 程序?qū)崿F(xiàn)正確性保障
3.1 可信編程規(guī)范
3.1.1 禁止使用的C語(yǔ)言特性
3.1.2 語(yǔ)言使用規(guī)則
3.1.3 領(lǐng)域相關(guān)規(guī)則
3.1.4 環(huán)境相關(guān)規(guī)則
3.1.5 檢測(cè)工具介紹
3.2 數(shù)值性質(zhì)分析技術(shù)
3.2.1 基于抽象解釋的數(shù)值性質(zhì)分析技術(shù)
3.2.2 區(qū)間抽象域的基本定義及操作
3.2.3 區(qū)間抽象域的冪集拓展
3.2.4 基于浮點(diǎn)區(qū)間冪集的程序分析方法
3.3 數(shù)據(jù)競(jìng)爭(zhēng)預(yù)防和檢測(cè)技術(shù)
3.3.1 典型數(shù)據(jù)競(jìng)爭(zhēng)案例及分析
3.3.2 避免數(shù)據(jù)競(jìng)爭(zhēng)的設(shè)計(jì)策略
3.3.3 數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)方法及工具
3.4 單元測(cè)試用例自動(dòng)生成技術(shù)
3.4.1 測(cè)試技術(shù)
3.4.2 應(yīng)用實(shí)例
3.5 數(shù)字虛擬仿真測(cè)試技術(shù)
3.5.1 數(shù)字虛擬仿真測(cè)試平臺(tái)的功能
3.5.2 數(shù)字虛擬仿真測(cè)試平臺(tái)構(gòu)建技術(shù)
3.5.3 數(shù)字虛擬仿真測(cè)試平臺(tái)
第4章 嵌入式軟件形式化驗(yàn)證
4.1 模型檢驗(yàn)
4.1.1 軟件模型檢驗(yàn)技術(shù)
4.1.2 嵌入式軟件模型檢驗(yàn)技術(shù)
4.1.3 模型檢驗(yàn)工具
4.1.4 面向源程序的模型檢驗(yàn)應(yīng)用舉例
4.2 定理證明
4.2.1 定理證明技術(shù)
4.2.2 嵌入式操作系統(tǒng)的形式化驗(yàn)證舉例
第5章 嵌入式軟件可信保障集成環(huán)境
5.1 集成環(huán)境的需求和功能
5.2 集成環(huán)境的集成方法
5.2.1 集成對(duì)象
5.2.2 集成方法
5.3 集成環(huán)境實(shí)現(xiàn)
5.3.1 集成環(huán)境體系架構(gòu)
5.3.2 集成環(huán)境的實(shí)現(xiàn)技術(shù)
5.3.3 設(shè)計(jì)實(shí)現(xiàn)
5.3.4 工具集成與應(yīng)用舉例
縮略語(yǔ)
參考文獻(xiàn)