检索结果-内蒙古大学图书馆

小型微型计算机系统 2015年第9期36卷 2125-2129页

作者：霍燕燕关永李晓娟王瑞张杰魏洪兴高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室首都师范大学信息工程学院北京100048 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191

大规模集成电路工艺技术的飞跃发展,掀起了计算机快速发展广泛普及的浪潮,同时又向计算机网络、巨型计算机、智能化方向以及分布式实时处理方向发展.其中,分布式实时系统的需求在各个领域的需求都不断扩大,于是,分布式实时操作系统也随... 详细信息

大规模集成电路工艺技术的飞跃发展,掀起了计算机快速发展广泛普及的浪潮,同时又向计算机网络、巨型计算机、智能化方向以及分布式实时处理方向发展.其中,分布式实时系统的需求在各个领域的需求都不断扩大,于是,分布式实时操作系统也随之产生.为了保证设计的可靠性和正确性,通过模型检测的方法对分布式实时操作系统的任务调度建立马尔科夫决策过程(MDP)模型,并以机器人分布式实时操作系统为例,用概率计算树逻辑(PCTL)对一些关键属性进行描述,通过PRISM平台对任务的可调度性进行验证和分析.通过将验证和分析得到的量化结果不断反馈给设计人员,以反馈得到的结果为依据,设计人员可以作出相应的策略,进一步提高设计的可靠性和正确性.

关键词：分布式实时操作系统任务调度概率模型检测马尔科夫决策过程 PRISM

来源：评论

学校读者我要写书评

暂无评论

RGMP-ROS混合机器人操作系统节点间通信的形式化验证

引用

小型微型计算机系统 2015年第10期36卷 2379-2383页

作者：王亚王瑞关永魏洪兴李晓娟张杰高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室首都师范大学信息工程学院北京100048 北京航空航天大学机械工程及自动化学院北京100191 北京化工大学信息科学与技术学院北京100029

在机器人研发领域,通过将ROS机器人操作系统移植到Linux操作系统上可以解决工业机器人控制器软件模块化问题,但是,运行在Linux系统上的ROS不具有实时性,无法满足机器人运动的实时控制需求.RGMP-ROS是一个应用于工业机器人控制器的混合... 详细信息

在机器人研发领域,通过将ROS机器人操作系统移植到Linux操作系统上可以解决工业机器人控制器软件模块化问题,但是,运行在Linux系统上的ROS不具有实时性,无法满足机器人运动的实时控制需求.RGMP-ROS是一个应用于工业机器人控制器的混合操作机器人系统,它能够解决ROS系统移植到Linux系统后的非实时性问题.因此,对RGMP-ROS混合操作系统的实时性验证有重要的意义.本文提出运用模型检测方法对RGMP-ROS系统节点间的通信进行验证.首先,对节点通信过程中的各部分建立时间自动机模型.然后用计算树逻辑公式对节点之间通信的可达性以及通信时间进行了形式化描述.最后在模型检测工具Uppaal中进行了验证.验证结果表明了RGMP-ROS系统具有实时性,可以满足实时性的需求.

关键词： RGMP-ROS 节点通信时间自动机计算树逻辑 Uppaal

来源：评论

学校读者我要写书评

暂无评论

结合属性重要度和灰色关联度的数据补齐方法

引用

计算机工程与设计 2014年第1期35卷 248-254页

作者：王方心潘巍吴立锋金声震李晓娟首都师范大学信息工程学院北京100048 首都师范大学高可靠嵌入式系统技术北京市工程研究中心北京100048 首都师范大学电子系统可靠性技术北京市重点实验室北京100048

结合属性重要度和灰色关联度,提出了一种新的数据补齐方法,可使补齐后的数据具有更高的识别率和分类性能。按照属性重要度确定各个条件属性的补齐顺序;对于当前要补齐的缺失样本,将所有完备样本分别与其进行比较,并选择灰色关联度最大... 详细信息

结合属性重要度和灰色关联度,提出了一种新的数据补齐方法,可使补齐后的数据具有更高的识别率和分类性能。按照属性重要度确定各个条件属性的补齐顺序;对于当前要补齐的缺失样本,将所有完备样本分别与其进行比较,并选择灰色关联度最大的完备样本对该样本的缺失数据进行补齐。并提出了一种新的判断数据补齐性能的评价标准,即补齐后的数据不能影响原有数据的识别率。实验结果表明,即使在很高的数据缺失比率下,该方法仍能很好地进行补齐,并能取得较高的识别率。

关键词：不完备数据补齐属性重要度补齐顺序灰色关联度评价标准

来源：评论

学校读者我要写书评

暂无评论

功率MOSFET寄生电容劣化对开关瞬态响应的影响

引用

电源技术 2014年第4期38卷 661-664页

作者：戴宇晟王国辉关永吴立锋李晓娟首都师范大学信息工程学院北京100048 首都师范大学高可靠嵌入式系统技术北京市工程研究中心北京100048 首都师范大学电子系统可靠性技术北京市重点实验室北京100048

为解决功率MOSFET寄生电容劣化影响寿命的问题,在MOSFET非线性模型基础上,深入分析MOSFET寄生电容参数和开关管瞬态响应信号之间的关系,推导了各参数和瞬态响应之间的关系表达式,并用Saber仿真实验进行验证。由于栅极对MOSFET的性能影... 详细信息

为解决功率MOSFET寄生电容劣化影响寿命的问题,在MOSFET非线性模型基础上,深入分析MOSFET寄生电容参数和开关管瞬态响应信号之间的关系,推导了各参数和瞬态响应之间的关系表达式,并用Saber仿真实验进行验证。由于栅极对MOSFET的性能影响至关重要,所以此次实验分析了和栅极相关的栅源电容Cgs和栅漏电容Cgd。结果表明,在寄生参数相同劣化程度时,栅源电容对瞬态响应的影响达到7.08%,而栅漏电容近似只有1.6%。栅源电容的劣化更大程度上影响瞬态响应,为MOSFET劣化提供了新的研究思路。

关键词： MOSFET 寄生电容瞬态响应软件仿真

来源：评论

学校读者我要写书评

暂无评论

非确定性环境中移动机器人实时避障的概率模型检测

引用

小型微型计算机系统 2014年第9期35卷 2104-2109页

作者：王铭王瑞李晓娟关永张杰魏洪兴高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室首都师范大学信息工程学院北京100048 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191

移动机器人的避障问题是机器人学的重要问题,实时避障是移动机器人安全导航的关键.针对移动机器人存在的制动机误差和传感器噪声等不确定因素,采用概率模型检测的方法对实时避障控制策略进行验证和定量分析.首先,将目标机器人的避障运... 详细信息

移动机器人的避障问题是机器人学的重要问题,实时避障是移动机器人安全导航的关键.针对移动机器人存在的制动机误差和传感器噪声等不确定因素,采用概率模型检测的方法对实时避障控制策略进行验证和定量分析.首先,将目标机器人的避障运动及动态障碍物的非确定运动建模为马尔科夫决策过程,其中避障策略包括等待避障、减速避障和加速避障.然后,运用概率计算树逻辑语言描述目标机器人运动的关键属性并使用概率模型检测工具进行验证.最后,分析得到目标机器人与动态障碍物发生碰撞的最大概率值;目标机器人采取减速(加速)避障时,减速(加速)行驶的最佳时间;目标机器人的控制误差对避障运动的影响等.实验结果表明某些参数影响目标机器人的避障效果,并为参数值的选择提供参考依据.

关键词：移动机器人控制误差实时避障概率模型检测马尔科夫决策过程

来源：评论

学校读者我要写书评

暂无评论

运用定理证明器ACL2验证机器人操作系统ROS节点间通信

引用

小型微型计算机系统 2014年第9期35卷 2126-2130页

作者：高雅李晓娟关永王瑞张杰魏洪兴高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室首都师范大学信息工程学院北京100048 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191

作为一种开源的机器人操作系统,ROS在家用或服务性机器人上也得到广泛应用,保证其设计的正确性相当重要.本文通过定理证明的方法对ROS的节点间通信进行形式化建模与属性验证.对通信层的节点间连接建立和消息传递过程进行抽象建模,模型... 详细信息

作为一种开源的机器人操作系统,ROS在家用或服务性机器人上也得到广泛应用,保证其设计的正确性相当重要.本文通过定理证明的方法对ROS的节点间通信进行形式化建模与属性验证.对通信层的节点间连接建立和消息传递过程进行抽象建模,模型融合网络拓扑、主题匹配和路由机制等部分,定义函数对其进行描述,提取路由函数的存在性、可达性及正确性等3个关键属性,运用定理证明工具ACL2对ROS节点间通信的功能正确性进行自动验证,证明消息从源节点出发并选择有效的传输路径到达目的节点.这种满足属性要求的参数化模型具有一般性和易扩展性,并能保证ROS节点间通信的终止属性和功能正确性,可为ROS通信层设计的正确性验证工作提供一个有效的方法参考.

关键词： ROS ACL2 定理证明参数化自动验证

来源：评论

学校读者我要写书评

暂无评论

一个空间线段距离算法的形式化和应用

一个空间线段距离算法的形式化和应用

引用

第八届全国测试学术会议

作者：安育龙施智平叶世伟李晓娟关永张杰魏洪兴高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室首都师范大学信息工程学院北京100048 中国科学院研究生院信息科学与工程学院北京100049 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191

对机器人控制算法进行验证工作,对于保障机器人安全工作具有重要意义.本文给出了一个可以在双臂机器人无碰撞运动规划中应用的空间线段距离算法,并完成了对这个算法正确性的形式化验证.本文中的形式化验证工作在定理证明器HOL4中实现,... 详细信息

对机器人控制算法进行验证工作,对于保障机器人安全工作具有重要意义.本文给出了一个可以在双臂机器人无碰撞运动规划中应用的空间线段距离算法,并完成了对这个算法正确性的形式化验证.本文中的形式化验证工作在定理证明器HOL4中实现,包括基本几何定义和定理的表示和证明,基于霍尔逻辑将算法表示成待证明的目标以及对这个目标的证明.

关键词：机器人无碰撞运动规划空间线段距离算法形式化验证

来源：评论

学校读者我要写书评

暂无评论

超级电容建模现状及展望

引用

电子元件与材料 2013年第8期32卷 5-10页

作者：单金生吴立锋关永王国辉李晓娟首都师范大学信息工程学院北京100048 首都师范大学高可靠嵌入式系统技术北京市工程研究中心北京100048 首都师范大学电子系统可靠性技术北京市重点实验室北京100048

介绍了超级电容的特点和工作原理,从物理结构,电气特性以及阻抗特性三个方面对现有的超级电容应用模型予以概述,给出了各类模型的建模依据;分析了各类模型的特点及其优缺点;阐述了各类模型的适用范围。最后,结合超级电容在实际应用中出... 详细信息

介绍了超级电容的特点和工作原理,从物理结构,电气特性以及阻抗特性三个方面对现有的超级电容应用模型予以概述,给出了各类模型的建模依据;分析了各类模型的特点及其优缺点;阐述了各类模型的适用范围。最后,结合超级电容在实际应用中出现的问题,展望了未来超级电容建模的发展趋势。

关键词：超级电容模型物理结构电气特性阻抗特性漏电流

来源：评论

学校读者我要写书评

暂无评论

超级电容容量动态测试系统设计

引用

计算机工程与设计 2013年第12期34卷 4374-4378页

作者：郝美娟吴立锋关永潘巍唐武兵李晓娟首都师范大学信息工程学院北京 100048 首都师范大学高可靠嵌入式系统技术北京市工程研究中心北京 100048 首都师范大学电子系统可靠性技术北京市重点实验室北京 100048

为了深入研究超级电容的容量与端电压、充放电电流的关系,设计并实现了基于LabVIEW的超级电容容量动态测试系统。对超级电容容量的测试方法、信号调理电路的设计、传感器及数据采集卡的选型进行了介绍,详细阐述了基于LabVIEW的软件设计... 详细信息

为了深入研究超级电容的容量与端电压、充放电电流的关系,设计并实现了基于LabVIEW的超级电容容量动态测试系统。对超级电容容量的测试方法、信号调理电路的设计、传感器及数据采集卡的选型进行了介绍,详细阐述了基于LabVIEW的软件设计,着重分析了超级电容端电压随时间的变化情况,并在此基础上研究了超级电容容量随端电压及充放电电流的变化情况。系统测试结果表明,该系统可以准确、同步地采集超级电容特征数据,确定端电压、充放电电流对超级电容容量的影响。

关键词：超级电容容量 LabVIEW数据采集系统设计

来源：评论

学校读者我要写书评

暂无评论

SpaceWire协议的形式化建模与概率分析

引用

小型微型计算机系统 2013年第9期34卷 2025-2029页

作者：李月星李晓娟关永王瑞张杰魏洪兴高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室首都师范大学信息工程学院北京100048 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191

SpaceWire是应用于航空航天领域的高速通信总线标准,保证其设计的可靠性和正确性至关重要.本文通过概率模型检测的方法对SpaceWire的交换层设计进行形式化建模与量化分析.基于马尔科夫决策过程(MDP)对交换层的链路初始化及正常运行过程... 详细信息

SpaceWire是应用于航空航天领域的高速通信总线标准,保证其设计的可靠性和正确性至关重要.本文通过概率模型检测的方法对SpaceWire的交换层设计进行形式化建模与量化分析.基于马尔科夫决策过程(MDP)对交换层的链路初始化及正常运行过程建立形式化概率模型,模型包括发送方、接收方和信道,提取SpaceWire交换层的4个关键属性,用概率计算树逻辑(PCTL)进行描述,运用PRISM平台对SpaceWire交换层设计进行验证和分析;并获得信道丢包概率不同情况下,链路初始化成功以及正常运行时数据包正确传输的概率,这种定量形式化分析结果可为SpaceWire的设计和实现提供参考依据.

关键词： SpaceWire 概率模型检测马尔科夫决策过程 PRISM

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：