首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   1篇
  免费   0篇
  国内免费   1篇
自动化技术   2篇
  2020年   1篇
  2017年   1篇
排序方式: 共有2条查询结果,搜索用时 15 毫秒
1
1.
基于Event-B的航天器内存管理系统形式化验证   总被引:1,自引:1,他引:0  
乔磊  杨孟飞  谭彦亮  蒲戈光  杨桦 《软件学报》2017,28(5):1204-1220
内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会较之前的验证工作带来更多难题,主要体现在:内存管理模块中的复杂数据结构的形式化描述;操作的规范语义;行为的建模;内部函数的规范及断言定义与循环不变式的定义;实时性验证等方面.本文拟针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法,来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.本文研究成果有望被直接应用于我国新一代的航天器系统上.  相似文献   
2.
软故障恢复设计对提高星载控制计算机系统可靠性非常重要,尤其在通信、遥感等长期空间任务中。星载控制计算机处理器模块(PM)采用了软故障恢复设计,而输入输出模块(IOP)未采用。提出了一种基于软件调试支持单元的IOP故障检测和恢复方法,该方法利用IOP的软件可定义特性,通过PM对IOP进行调试,实现其内存恢复和程序存储器刷新等,从而完成IOP的故障恢复。该设计已应用到通信、遥感等长期任务的星载控制计算机中。地面试验和分析结果表明,该恢复设计可覆盖绝大部分软故障及部分硬故障,具有较高的可靠性,可以应用于星载控制计算机的在轨故障修复。  相似文献   
1
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号