摘要：中国空间站的建立为国产先进制程芯片提供了真实的在轨飞行验证条件。为实现不同种类、不同型号国产先进制程电子元器件在空间辐射环境中的验证,设计了一种通用的在轨飞行验证系统。系统采用“主控单元+试验单元”的平台架构,运用在轨可更换模块和可重构的系统设计,支持航天员定期在轨更换试验模块以完成验证任务的在轨升级。文中给出系统的硬件设计、软件数据管理机制以及在轨飞行验证结果。结果表明,该系统设计有效,成功完成了16 nm FinFET、28 nm亿门级FPGA、高速DAC等10类20余款国产先进制程芯片的在轨工作监测,可为国产先进制程芯片空间适用性研究提供参考。

摘要：在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而,中断在并发语义、同步机制、调度机制等方面与线程(任务)有诸多不同,具有Ad-hoc特征,难以统一刻画,因此,主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争案例库为基础进行了系统分析,提出刻画有害中断数据竞争的7种缺陷模式.针对其中最常见且最难解决的单变量访问序模式,基于抽象解释,提出一种支持过程间分析、中断并发分析的高效检测方法.设计并实现了相应的检测工具Space DRC.实验结果表明,Space DRC能够在145ms内检测出约21 400行程序中的真实数据竞争.Space DRC已经在多个航天重点型号中进行了应用,使得中断数据竞争专项分析的效率提高了至少5倍,并且降低了问题遗漏率.

摘要：针对数据访问冲突问题的检测方法及工具的研究很多,但缺少对其进行评估的基准测试集。文章基于大量真实航天嵌入式软件中断数据访问冲突案例研究的结果,总结出影响数据访问冲突检测的6类要素,设计开发了嵌入式软件中断数据访问冲突基准测试集程序RaceBench,对SpaceDRC工具进行了指标评估。结果表明,RaceBench能够有效评估工具的适用性。

摘要：基于ZYNQ7000全可编程SoC,对EMMC的应用进行了深入地分析和研究。首先从硬件配置说明了EMMC的引脚分配,然后结合寻址方式和数据传输模式对EMMC的软件操作流程进行阐述。此方案在精简了存储器设计、保证数据安全性的前提下,满足了实际功能需求,具有重要的理论意义及工程实际应用价值。

摘要：根据统计,数组越界是航天嵌入式软件开发过程中出现最多且最容易被遗漏的缺陷类型之一.目前自动化检测数组越界多基于抽象解释、符号执行、程序模型检验等方法,这些方法在误报、漏报、可扩展性等方面的表现依赖于软件及缺陷特征.分析了近三年航天嵌入式软件第三方测试中发现的94个数组越界问题,从缺陷模式和缺陷表现形式两方面分析得出10项航天嵌入式软件数组越界缺陷特征,并提出对设计具体检测方法关键的若干启示.进一步基于这些特征和启示探讨了数组越界检测算法针对中断驱动型程序的改进方向.