期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到4篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
基于Event-B的航天器内存管理系统形式化验证 被引量：13
1
作者 乔磊 杨孟飞 +2 位作者 谭彦亮 蒲戈光 杨桦 《软件学报》 EI CSCD 北大核心 2017年第5期1204-1220,共17页
内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂... 内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会比之前的验证工作带来更多难题,主要体现在:内存管理模块中的复杂数据结构的形式化描述,操作的规范语义,行为的建模,内部函数的规范及断言定义与循环不变式的定义,实时性验证等方面.针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.该研究成果有望直接应用于我国新一代的航天器系统. 展开更多
关键词 航天器操作系统 内存管理 形式化验证
下载PDF
基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证 被引量：4
2
作者 谭彦亮 杨桦 乔磊 《空间控制技术与应用》 2014年第4期57-62,共6页
随着中国航天技术的发展,航天器系统的软件规模越来越大、复杂度越来越高,对航天软件的正确性、可靠性、安全性等提出了更为严格的要求.形式化方法是提高软件可信性的一个重要途径.利用形式化方法 Event-B对嵌入式操作系统SpaceOS2的任... 随着中国航天技术的发展,航天器系统的软件规模越来越大、复杂度越来越高,对航天软件的正确性、可靠性、安全性等提出了更为严格的要求.形式化方法是提高软件可信性的一个重要途径.利用形式化方法 Event-B对嵌入式操作系统SpaceOS2的任务管理模块的进行需求建模,依靠不变式来保证模型的正确性,并且在Rodin平台上对模型进行了形式化验证,结果表明模型是正确的. 展开更多
关键词 任务管理 形式化模型 形式化验证 Event—B
下载PDF
一种基于虚拟页地址映射的NAND Flash管理算法 被引量：3
3
作者 许娜 彭飞 +2 位作者 谭彦亮 苗志富 曹梦丹 《空间控制技术与应用》 CSCD 北大核心 2020年第3期60-65,共6页
本文提出了一种基于虚拟页地址映射的NAND Flash管理算法.该算法通过定义坏块表、对应表等结构,以及设计的坏块替换策略和虚拟页地址到实际物理页地址的转换算法,实现上层软件采用虚拟地址对NAND Flash的无坏块连续页地址访问.该算法是... 本文提出了一种基于虚拟页地址映射的NAND Flash管理算法.该算法通过定义坏块表、对应表等结构,以及设计的坏块替换策略和虚拟页地址到实际物理页地址的转换算法,实现上层软件采用虚拟地址对NAND Flash的无坏块连续页地址访问.该算法是一种高效的地址映射算法,能高效地对数据进行索引,占用SRAM空间较少,使系统达到高性能,并使得闪存使用的更加稳定持久. 展开更多
关键词 NAND Flash 虚拟页 地址映射
下载PDF
基于调试支持单元的星载控制计算机软故障恢复设计 被引量：1
4
作者 刘波 于广良 +3 位作者 徐建 谭彦亮 江耿丰 李建平 《测控技术》 2020年第1期42-45,共4页
软故障恢复设计对提高星载控制计算机系统可靠性非常重要,尤其在通信、遥感等长期空间任务中。星载控制计算机处理器模块(PM)采用了软故障恢复设计,而输入输出模块(IOP)未采用。提出了一种基于软件调试支持单元的IOP故障检测和恢复方法... 软故障恢复设计对提高星载控制计算机系统可靠性非常重要,尤其在通信、遥感等长期空间任务中。星载控制计算机处理器模块(PM)采用了软故障恢复设计,而输入输出模块(IOP)未采用。提出了一种基于软件调试支持单元的IOP故障检测和恢复方法,该方法利用IOP的软件可定义特性,通过PM对IOP进行调试,实现其内存恢复和程序存储器刷新等,从而完成IOP的故障恢复。该设计已应用到通信、遥感等长期任务的星载控制计算机中。地面试验和分析结果表明,该恢复设计可覆盖绝大部分软故障及部分硬故障,具有较高的可靠性,可以应用于星载控制计算机的在轨故障修复。 展开更多
关键词 星载控制计算机 软故障 故障恢复 调试支持单元
下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部