航天器控制应用的星载计算机技术

介绍了中国研制的用于近地轨道、太阳同步轨道和地球同步轨道航天器的几种主要星载容错计算机的功能和主要特点以及它们的容错结构,并简述了星载控制计算机的发展趋势。     

基于FPGA中CLB结构模型的内部进化及其容错

内部进化是研究在线可进化硬件的方法,可用于实现容错、自适应的航天器硬件系统.现场可编程门阵列(FPGA,Field Programmable Gate Array)是目前实现数字电路进化的主要可编程逻辑器件.本文分析了FPGA的结构特点,对其基本组成单元可配置逻辑块(CLB,Configurable Logic Block)的结构进行了简化,提出一种可编程逻辑器件模型,设计了一种基于该模型的内部进化方法,并实现了一个内部进化系统.采用故障注入的方法对内部进化的容错特性进行了研究,讨论了可进化硬件实现容错的条件.     

形式验证中ROBDD变量排序算法的研究

不良的ROBDD变量排序会引发状态空间爆炸的危机,从而影响形式验证方法的推广和使用。通过对CUDD数据包中ROBDD遗传变量排序算法的研究,利用变异操作和保留最优个体的时代繁殖操作对原算法进行了改进。实验数据表明,改进后的算法在可以容忍的运行时间内减少了ROBDD的节点数目,在一定程度上缓解了形式验证中状态空间爆炸的危机。     

应用于实时系统中存储器故障测试的一种新方法

针对实时存储器系统的常见故障类型提出了一种新的存储器测试方法,其最大特点是在测试过程中不使用缓冲区,从而节省了系统资源,增加了测试覆盖率;同时证明了该存储器测试方法的正确性。     

80系列容错存储器设计的方法及可靠性分析

通过对一类在市场上广泛应用且在空间上使用的处理机系列──８０系列的分析,提出了一种实现存储器容错的新方法。这种方法不需要切换控制电路,提高了系统的可靠性。文章分析了这种方法的可实现性,并举例说明。最后,对它的可靠性进行了分析,并给出在同样的冗余下,它与备份形式的存储器容错结构的可靠性比较结果。     

基于有限状态机的操作系统需求层形式化验证

操作系统是航天器必备的基本软件，操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障，但仍存在不能完全排除缺陷的情况，因此对空间操作系统开展形式化验证研究势在必行.需求层验证是操作系统形式化验证的一部分，本文在分析操作系统需求的基础上，采用有限状态机在操作系统需求层进行形式化描述，并针对应用在某航天器上的SpaceOS2在需求层进行了建模，相应地在定理证明工具Coq中进行了描述建模；然后定义了六条操作系统应满足的全局性质并进行了形式化描述，给出了系统模型满足这些性质的机器可检查的证明.证明结果表明采用有限状态机方法对操作系统需求层进行形式化验证是可行的，为进一步全面形式化验证奠定了基础.     

一种增强SR模型适应性的方法

 通过对软件可靠性(SR)模型拟合曲线的分析,提出模型固有特征是影响SR模型适应性的因素之一,在此基础上,提出构建模型组以增强SR模型适应性的新方法。实践表明,该方法是可行的。     

基于可进化硬件的容错技术及其原理

可进化硬件容错技术是一种模仿生物进化过程的容错方法,现已成为世界各国容错计算技术领域新的研究方向。可进化硬件不是采用传统的静态冗余技术,而是利用其本身固有的特性实现容错。重点论述可进化硬件技术的2个基本要素,并分析其实现容错的原理。     

空间容错计算机的基本问题和对策

本文从分折空间应用环境对计算机的要求入手，指出研制这类系统所遇到的主要问题，提出解决这些问题的基本技术和措施。     

三模冗余MPSOC容错设计与验证

为了提高MPSOC处理器的可靠性,提出了一种基于软件表决和硬件仲裁的三模冗余容错处理器设计方案,并对这种容错设计进行了原型实现和验证,试验结果表明了方案的正确性和有效性.