期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到4篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
SpaceOS中若干全局性质的形式化描述和验证 被引量：8
1
作者 顾海博 付明 +1 位作者 乔磊 冯新宇 《小型微型计算机系统》 CSCD 北大核心 2019年第1期141-148,共8页
SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件,是影响航天任务成败的关键因素. SpaceOS在设计中提出了一些多个内核模块(如任务管理、调度、通信和时... SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件,是影响航天任务成败的关键因素. SpaceOS在设计中提出了一些多个内核模块(如任务管理、调度、通信和时间管理等)相互协同过程中所需要满足的全局性质.本文扩展已有的操作系统验证框架支持全局性质的推理,为SpaceOS内核建立抽象模型,给出主要系统调用的抽象规范,并基于设计需求给出形式化定义描述若干全局性质,通过严格的数学证明保证SpaceOS在抽象设计层面上满足这些全局性质.所有工作都在证明助手Coq中完成. 展开更多
关键词 spaceos 形式化验证 全局性质 操作系统内核 COQ
在线阅读 下载PDF
基于SpaceOS2的TCP/IP网络协议栈移植 被引量：4
2
作者 袁瑞成 刘波 +1 位作者 乔磊 刘健培 《空间控制技术与应用》 CSCD 北大核心 2018年第4期46-55,共10页
航天器专用网络平台是未来航天器组网协同工作完成更复杂任务的关键技术.在操作系统层面需要对其进行有效地支持,以更好地提供给空间应用程序灵活和可靠的数据通讯服务.将伯克利BSD的TCP/IP网络协议栈的基础协议部分移植到航天器嵌入式... 航天器专用网络平台是未来航天器组网协同工作完成更复杂任务的关键技术.在操作系统层面需要对其进行有效地支持,以更好地提供给空间应用程序灵活和可靠的数据通讯服务.将伯克利BSD的TCP/IP网络协议栈的基础协议部分移植到航天器嵌入式操作系统SpaceOS2上,用以替代VxWorks操作系统.叙述协议系统中传输层的设计过程和模块接口的移植过程,并给出在SPARC处理器硬件平台上的性能测试结果. 展开更多
关键词 网络协议 spaceos2 TCP/IP
在线阅读 下载PDF
基于SQL-92和JDBC的SpaceOS数据库数据迁移的实现 被引量：2
3
作者 宁泰安 刘金刚 《计算机应用与软件》 CSCD 北大核心 2014年第12期64-67,190,共5页
针对Space操作系统的Postgre SQL数据库能对异构关系数据库进行数据迁移的需求,在SQL-92和JDBC基础上,介绍异构数据迁移时元数据和记录数据处理的主要流程,并设计了以表示层、元数据层、业务逻辑层和数据访问层为结构的数据迁移模块。... 针对Space操作系统的Postgre SQL数据库能对异构关系数据库进行数据迁移的需求,在SQL-92和JDBC基础上,介绍异构数据迁移时元数据和记录数据处理的主要流程,并设计了以表示层、元数据层、业务逻辑层和数据访问层为结构的数据迁移模块。详细分析了SQL声明前数据类型映射和代理主键值映射这两个关键步骤的算法实现。数据迁移模块在JDK1.6环境下实现。通过对异构数据库与Postgre SQL间进行数据迁移实验,验证了迁移模块是合理而有效的,具有良好的通用性和兼容性。 展开更多
关键词 spaceos PostgreSQL异构数据库 数据迁移SQL-92 JDBC
在线阅读 下载PDF
基于SpaceOS的工控机跨平台SMP多核移植与应用
4
作者 张潇锐 徐建 +4 位作者 谭彦亮 李明洋 韩朝君 张锦坤 李振 《电子技术应用》 2026年第3期113-120,共8页
面向航天及工业控制等领域计算机实时性要求高、数据处理量大、通信速度快、运行任务复杂等需求,采用可编程融合芯片实现基于星载计算机实时操作系统SpaceOS的跨平台SMP多核移植。首先,选用FMQL45作为软硬件平台,移植SpaceOS操作系统,... 面向航天及工业控制等领域计算机实时性要求高、数据处理量大、通信速度快、运行任务复杂等需求,采用可编程融合芯片实现基于星载计算机实时操作系统SpaceOS的跨平台SMP多核移植。首先,选用FMQL45作为软硬件平台,移植SpaceOS操作系统,实现板级支持包、任务调度等功能。进一步,设计了一种基于FMQL45平台的多核SMP方案,进行多核内存分区、堆栈配置、中断响应、任务管理等,通过核间中断、共享内存等方式实现多核之间的同步与通信。最后,设计并实现典型的SMP多核工程,构建IAR开发环境与I-Jet调试器的调试体系,进行功能及性能测试,验证了系统的多核处理能力。 展开更多
关键词 spaceos操作系统 SMP多核 复旦微FMQL45 工控机
在线阅读 下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部