摘要：spaceos是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.spaceos作为底层系统软件,是影响航天任务成败的关键因素. spaceos在设计中提出了一些多个内核模块(如任务管理、调度、通信和时间管理等)相互协同过程中所需要满足的全局性质.本文扩展已有的操作系统验证框架支持全局性质的推理,为spaceos内核建立抽象模型,给出主要系统调用的抽象规范,并基于设计需求给出形式化定义描述若干全局性质,通过严格的数学证明保证spaceos在抽象设计层面上满足这些全局性质.所有工作都在证明助手Coq中完成.

摘要：针对Space操作系统的Postgre SQL数据库能对异构关系数据库进行数据迁移的需求,在SQL-92和JDBC基础上,介绍异构数据迁移时元数据和记录数据处理的主要流程,并设计了以表示层、元数据层、业务逻辑层和数据访问层为结构的数据迁移模块。详细分析了SQL声明前数据类型映射和代理主键值映射这两个关键步骤的算法实现。数据迁移模块在JDK1.6环境下实现。通过对异构数据库与Postgre SQL间进行数据迁移实验,验证了迁移模块是合理而有效的,具有良好的通用性和兼容性。

摘要：分析嵌入式实时操作系统在国内外深空探测领域的研究与应用现状，提出面向深空探测空间飞行器应用特点的具有多任务管理、内存管理、文件系统、容错和故障管理等功能的高可靠、高性能的嵌入式实时操作系统的研究与设计方案，并展望其在未来网络化及分布式安全深空探测空间飞行器中的发展前景。