期刊导航
期刊开放获取
vip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
3
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式：
文摘
详细
列表
相关度排序
被引量排序
时效性排序
SpaceOS中若干全局性质的形式化描述和验证
被引量：
7
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处理器硬件平台上的性能测试结果.
展开更多
关键词
网络协议
spaceos
2
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中若干全局性质的形式化描述和验证
被引量：
7
1
作者
顾海博
付明
乔磊
冯新宇
机构
中国科学技术大学计算机科学与技术学院
中国科学技术大学苏州研究院软件安全实验室
华为上海研究所
北京控制工程研究所
南京大学计算机软件新技术国家重点实验室
出处
《小型微型计算机系统》
CSCD
北大核心
2019年第1期141-148,共8页
基金
国家自然科学基金项目(61632005
61502031)资助
文摘
SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件,是影响航天任务成败的关键因素. SpaceOS在设计中提出了一些多个内核模块(如任务管理、调度、通信和时间管理等)相互协同过程中所需要满足的全局性质.本文扩展已有的操作系统验证框架支持全局性质的推理,为SpaceOS内核建立抽象模型,给出主要系统调用的抽象规范,并基于设计需求给出形式化定义描述若干全局性质,通过严格的数学证明保证SpaceOS在抽象设计层面上满足这些全局性质.所有工作都在证明助手Coq中完成.
关键词
spaceos
形式化验证
全局性质
操作系统内核
COQ
Keywords
spaceos
formal verification
global property
operating system kernel
Coq
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
基于SpaceOS2的TCP/IP网络协议栈移植
被引量：
4
2
作者
袁瑞成
刘波
乔磊
刘健培
机构
天津科技大学
北京控制工程研究所
北京邮电大学
出处
《空间控制技术与应用》
CSCD
北大核心
2018年第4期46-55,共10页
文摘
航天器专用网络平台是未来航天器组网协同工作完成更复杂任务的关键技术.在操作系统层面需要对其进行有效地支持,以更好地提供给空间应用程序灵活和可靠的数据通讯服务.将伯克利BSD的TCP/IP网络协议栈的基础协议部分移植到航天器嵌入式操作系统SpaceOS2上,用以替代VxWorks操作系统.叙述协议系统中传输层的设计过程和模块接口的移植过程,并给出在SPARC处理器硬件平台上的性能测试结果.
关键词
网络协议
spaceos
2
TCP/IP
Keywords
network protocol
spaceos
2
TCP/IP
分类号
TP393.1 [自动化与计算机技术—计算机应用技术]
在线阅读
下载PDF
职称材料
题名
基于SQL-92和JDBC的SpaceOS数据库数据迁移的实现
被引量：
2
3
作者
宁泰安
刘金刚
机构
首都师范大学计算机科学联合研究院
中国科学院计算技术研究所
出处
《计算机应用与软件》
CSCD
北大核心
2014年第12期64-67,190,共5页
文摘
针对Space操作系统的Postgre SQL数据库能对异构关系数据库进行数据迁移的需求,在SQL-92和JDBC基础上,介绍异构数据迁移时元数据和记录数据处理的主要流程,并设计了以表示层、元数据层、业务逻辑层和数据访问层为结构的数据迁移模块。详细分析了SQL声明前数据类型映射和代理主键值映射这两个关键步骤的算法实现。数据迁移模块在JDK1.6环境下实现。通过对异构数据库与Postgre SQL间进行数据迁移实验,验证了迁移模块是合理而有效的,具有良好的通用性和兼容性。
关键词
spaceos
PostgreSQL异构数据库
数据迁移SQL-92
JDBC
Keywords
spaceos
PostgreSQL Heterogeneous databases Data migration SQL-92 JDBC
分类号
TP311.132.2 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
SpaceOS中若干全局性质的形式化描述和验证
顾海博
付明
乔磊
冯新宇
《小型微型计算机系统》
CSCD
北大核心
2019
7
在线阅读
下载PDF
职称材料
2
基于SpaceOS2的TCP/IP网络协议栈移植
袁瑞成
刘波
乔磊
刘健培
《空间控制技术与应用》
CSCD
北大核心
2018
4
在线阅读
下载PDF
职称材料
3
基于SQL-92和JDBC的SpaceOS数据库数据迁移的实现
宁泰安
刘金刚
《计算机应用与软件》
CSCD
北大核心
2014
2
在线阅读
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部
