-
>
中共中央在西柏坡
-
>
中国历代政治得失
-
>
中国共产党的一百年
-
>
在庆祝中国共产主义青年团成立100周年大会上的讲话
-
>
中国的民主
-
>
中华人民共和国六十年实录(套装共10册)
-
>
新书)社会主义发展简史(大字本)
可信的航天嵌入式控制软件开发技术 版权信息
- ISBN:9787118112665
- 条形码:9787118112665 ; 978-7-118-11266-5
- 装帧:一般胶版纸
- 册数:暂无
- 重量:暂无
- 所属分类:>>
可信的航天嵌入式控制软件开发技术 本书特色
《可信的航天嵌入式控制软件开发技术》主要介绍航天嵌入式控制软件可信保障技术体系及其关键技术。首先从近年来的实际案例提炼出影响航天嵌入式软件可信性的十大可信问题,针对这些关键可信问题,从问题、阶段、方法、工具和度量五个维度进行研究,形成了具有五维体系结构的可信性保障技术体系;然后,重点论述了需求建模与验证、程序实现正确性保障、嵌入式软件形式化验证等关键问题的解决方案;*后依据可信保障技术体系的需求,介绍了构建嵌入式软件可信保障集成环境的集成方法、体系架构和关键技术。
《可信的航天嵌入式控制软件开发技术》针对嵌入式软件研制中的实际问题给出系统的解决方案,实用性强,对于在航天行业以及航空、兵器、汽车、核电等行业从事嵌入式软件研制的工程技术人员和系统总体设计人员,具有很好的参考价值。
可信的航天嵌入式控制软件开发技术 内容简介
本书主要论述了航天嵌入式软件可信保障的问题、解决方法和相关工具,并介绍了可信保障集成环境。本书由以下内容组成:嵌入式软件可信性保障技术体系;航天控制软件需求建模与验证;程序实现正确性保障;操作系统验证;航天嵌入式软件可信保障集成环境构建。
可信的航天嵌入式控制软件开发技术 目录
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 工具集成与应用举例
缩略语
参考文献
可信的航天嵌入式控制软件开发技术 作者简介
杨孟飞,现为国家某重点型号总设计师,博士生导师,国家有突出贡献中青年专家,享受政府特殊津贴,国家百千万人才工程第一第二层次人选。现任中国自动化学会副理事长,曾任中国计算机学会理事,中国宇航学会空间控制专业委员会主任,中国计算机学会工业控制专业委员会主任。主要从事控制计算机系统、控制系统及空间飞行器总体等方面的研究和研制工作。获国家发明二等奖一项,国家科技进步一等奖一项,省部级奖十项,发明专利20余项,发表学术论文60余篇。
- >
罗庸西南联大授课录
罗庸西南联大授课录
¥13.8¥32.0 - >
罗曼·罗兰读书随笔-精装
罗曼·罗兰读书随笔-精装
¥17.4¥58.0 - >
史学评论
史学评论
¥23.2¥42.0 - >
诗经-先民的歌唱
诗经-先民的歌唱
¥15.5¥39.8 - >
名家带你读鲁迅:故事新编
名家带你读鲁迅:故事新编
¥13.0¥26.0 - >
二体千字文
二体千字文
¥16.8¥40.0 - >
唐代进士录
唐代进士录
¥25.9¥39.8 - >
朝闻道
朝闻道
¥15.0¥23.8
-
辛亥革命专题研究丛书/湖南保路运动研究
¥10.6¥20 -
孙子兵法与三十六计
¥8.8¥18 -
孙子兵法
¥18.5¥30 -
大国威仪-中国人民解放军三军仪仗队60周年纪实
¥18¥68 -
这才是战争 将略
¥45.2¥68 -
毛泽东的艰难决策(一 中国人民志愿军出兵朝鲜的决策过程)
¥14.2¥26