可信的航天嵌入式控制软件开发技术_PDF下载[76MB-百度云]杨孟飞

本书特色

[

　　《可信的航天嵌入式控制软件开发技术》主要介绍航天嵌入式控制软件可信保障技术体系及其关键技术。首先从近年来的实际案例提炼出影响航天嵌入式软件可信性的十大可信问题，针对这些关键可信问题，从问题、阶段、方法、工具和度量五个维度进行研究，形成了具有五维体系结构的可信性保障技术体系；然后，重点论述了需求建模与验证、程序实现正确性保障、嵌入式软件形式化验证等关键问题的解决方案；*后依据可信保障技术体系的需求，介绍了构建嵌入式软件可信保障集成环境的集成方法、体系架构和关键技术。
　　《可信的航天嵌入式控制软件开发技术》针对嵌入式软件研制中的实际问题给出系统的解决方案，实用性强，对于在航天行业以及航空、兵器、汽车、核电等行业从事嵌入式软件研制的工程技术人员和系统总体设计人员，具有很好的参考价值。

]

第1章嵌入式软件可信性保障技术体系1．1 航天嵌入式控制系统的组成和特点1．2 航天嵌入式控制软件中的可信问题1．2．1 实时性问题1．2．2 内存使用问题1．2．3 数据使用问题1．2．4 计算问题1．2．5 协议正确性问题1．2．6 状态转换问题1．2．7 故障处理问题1．2．8 编译等价性问题1．2．9 编码问题1．2．10 各阶段一致性问题1．3 可信保障五维体系结构模型1．4 实例：时序保障问题分析1．4．1 需求分析阶段的保障1．4．2 设计阶段的保障1．4．3 编码阶段的保障1．4．4 测试阶段的保障1．4．5 方法、技术和工具1．4．6 度量第2章航天控制软件需求建模与验证2．1 需求建模语言2．1．1 建模语法定义2．1．2 建模语义解释2．2 需求性质描述语言2．2．1 性质描述语法定义2．2．2 性质描述语义解释2．2．3 性质描述模板2．3 分析与验证方法2．3．1 类型检查2．3．2 数据流分析2．3．3 原型生成与快速仿真2．3．4 随机语义2．3．5 概率模型检查2．4 SPRADL应用框架第3章程序实现正确性保障3．1 可信编程规范3．1．1 禁止使用的C语言特性3．1．2 语言使用规则3．1．3 领域相关规则3．1．4 环境相关规则3．1．5 检测工具介绍3．2 数值性质分析技术3．2．1 基于抽象解释的数值性质分析技术3．2．2 区间抽象域的基本定义及操作3．2．3 区间抽象域的幂集拓展3．2．4 基于浮点区间幂集的程序分析方法3．3 数据竞争预防和检测技术3．3．1 典型数据竞争案例及分析3．3．2 避免数据竞争的设计策略3．3．3 数据竞争检测方法及工具3．4 单元测试用例自动生成技术3．4．1 测试技术3．4．2 应用实例3．5 数字虚拟仿真测试技术3．5．1 数字虚拟仿真测试平台的功能3．5．2 数字虚拟仿真测试平台构建技术3．5．3 数字虚拟仿真测试平台第4章嵌入式软件形式化验证4．1 模型检验4．1．1 软件模型检验技术4．1．2 嵌入式软件模型检验技术4．1．3 模型检验工具4．1．4 面向源程序的模型检验应用举例4．2 定理证明4．2．1 定理证明技术4．2．2 嵌入式操作系统的形式化验证举例第5章嵌入式软件可信保障集成环境5．1 集成环境的需求和功能5．2 集成环境的集成方法5．2．1 集成对象5．2．2 集成方法5．3 集成环境实现5．3．1 集成环境体系架构5．3．2 集成环境的实现技术5．3．3 设计实现5．3．4 工具集成与应用举例缩略语参考文献