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

电子学报 2018年第11期46卷 2787-2796页

作者：张美玉张倩颖孟子琪施智平关永首都师范大学信息工程学院北京100048 成像技术北京市高精尖创新中心北京100048 轻型工业机器人与安全验证北京市重点实验室北京100048 电子系统可靠性技术北京市重点实验室北京100048

随着全球工业4. 0战略的提出,工业控制及航空航天等领域对嵌入式系统的要求越来越高,对实时性具有严格要求同时还需要应用功能丰富的通用操作系统的支持.针对该需求现状,学术界和产业界提出双操作系统的解决思路,即同时运行实时操作系... 详细信息

随着全球工业4. 0战略的提出,工业控制及航空航天等领域对嵌入式系统的要求越来越高,对实时性具有严格要求同时还需要应用功能丰富的通用操作系统的支持.针对该需求现状,学术界和产业界提出双操作系统的解决思路,即同时运行实时操作系统和通用操作系统.本文归纳总结国内外嵌入式双操作系统的研究现状,对各种实现技术进行深入探讨和分析,列举嵌入式双操作系统典型应用和主要应用领域,最后对该类技术的研究趋势进行总结.

关键词：双操作系统嵌入式操作系统实时性虚拟化双核

来源：评论

学校读者我要写书评

暂无评论

金属电磁带隙波导特性分析

引用

华中科技大学学报（自然科学版） 2007年第S1期35卷 27-29,33页

作者：柏宁丰孙小菡廖复疆冯进军东南大学电子系统可靠性研究中心江苏南京210096 大功率微波电真空器件技术国家重点实验室北京100016

利用有限差分(FDTD)法分析了两维金属电磁带隙(EBG)波导带隙、耦合频率和模场分布,确定了EBG结构参数和对应的频率范围;利用HFSS建立了金属电磁带隙结构分析模型,设计了带有矩形波导转换的EBG波导.基于HFSS分析该波导,得到了这两种结构... 详细信息

利用有限差分(FDTD)法分析了两维金属电磁带隙(EBG)波导带隙、耦合频率和模场分布,确定了EBG结构参数和对应的频率范围;利用HFSS建立了金属电磁带隙结构分析模型,设计了带有矩形波导转换的EBG波导.基于HFSS分析该波导,得到了这两种结构的传输谱线,对比说明矩形波导接口适用于窄带应用,而圆形波导接口适用于宽带应用.实验测试结果与数值分析符合较好.

关键词：电磁带隙 HFSS 波导

来源：评论

学校读者我要写书评

暂无评论

机器人碰撞检测方法形式化

引用

软件学报 2022年第6期33卷 2246-2263页

作者：陈善言关永施智平王国辉首都师范大学信息工程学院北京100048 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学) 北京100048 轻型工业机器人与安全验证北京市重点实验室(首都师范大学) 北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 高可靠嵌入式系统北京市工程研究中心(首都师范大学) 北京100048

为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以... 详细信息

为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.

关键词：机器人碰撞检测形式化方法定理证明 HOL-Light

来源：评论

学校读者我要写书评

暂无评论

软硬件协同设计的SEU故障注入技术研究

引用

电子学报 2018年第10期46卷 2534-2538页

作者：王晶荣金叶周继芹于航申娇张伟功首都师范大学信息工程学院北京100048 北京微电子技术研究所北京100076 首都师范大学电子系统可靠性技术北京市重点实验室北京100048

针对现有容错计算机故障注入方法缺乏对空间环境中频发的单粒子故障模型的支持,本文提出了一种利用背板技术的软硬件协同仿真与故障注入技术,分别针对寄存器部件和存储器部件的特性,设计了多位错误的单粒子故障模型,在寄存器传输级实现... 详细信息

针对现有容错计算机故障注入方法缺乏对空间环境中频发的单粒子故障模型的支持,本文提出了一种利用背板技术的软硬件协同仿真与故障注入技术,分别针对寄存器部件和存储器部件的特性,设计了多位错误的单粒子故障模型,在寄存器传输级实现了通过软件生成故障并注入到硬件设计中的软硬件协同故障注入方案,避免了在硬件设计中修改代码生成故障破坏系统完整性的问题.基于Leon2内核的故障注入实验表明,本文设计的平台为处理器容错设计提供了一个自动化、非侵入、低开销的故障注入和可靠性评估方案.

关键词：容错故障注入软硬件协同单粒子翻转微处理器寄存器传输级

来源：评论

学校读者我要写书评

暂无评论

以太坊中间语言的可执行语义

引用

软件学报 2021年第6期32卷 1717-1732页

作者：韩宁李希萌张倩颖王国辉施智平关永首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 北京成像理论与技术高精尖创新中心(首都师范大学) 北京100048

智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以... 详细信息

智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义(executable semantics),由120个Yul语言程序组成的测试集进行测试.该工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.

关键词：智能合约 Yul语言 Isabelle/HOL 形式化语义以太坊

来源：评论

学校读者我要写书评

暂无评论

基于函数式语义的循环和递归程序结构通用证明技术

引用

软件学报 2023年第8期34卷 3686-3707页

作者：李希萌王国辉张倩颖施智平关永首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 北京成像理论与技术高精尖创新中心(首都师范大学) 北京100048

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明... 详细信息

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.

关键词：程序验证大步操作语义定理证明 Coq定理证明器

来源：评论

学校读者我要写书评

暂无评论

自适应双路间隔调控跟踪算法

引用

计算机应用与软件 2023年第1期40卷 173-183页

作者：蒋秋萍付小雁首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室北京100048

卷积特征可有效解决复杂场景下的跟踪漂移问题,但特征提取耗时较长;传统手工算法跟踪速度快,然而精度有待提高。基于此,提出自适应双路间隔调控算法。针对目标尺度变化问题,使用多尺度特征训练跟踪器并依据质量评估自适应融合结果,为减... 详细信息

卷积特征可有效解决复杂场景下的跟踪漂移问题,但特征提取耗时较长;传统手工算法跟踪速度快,然而精度有待提高。基于此,提出自适应双路间隔调控算法。针对目标尺度变化问题,使用多尺度特征训练跟踪器并依据质量评估自适应融合结果,为减少计算开销采用主成分分析降维;算法实时评估目标运动状态,在手工主线算法基础上间隔性地调用深度算法,在保证跟踪精度的同时尽可能地减少时间消耗。实验表明该算法实现了特征优势互补,精度可达0.91,GPU速度17.5 FPS。

关键词：相关滤波多尺度质量评估深度卷积特征双路间隔调控策略

来源：评论

学校读者我要写书评

暂无评论

基于深度学习的音频抑郁症识别

引用

计算机应用与软件 2019年第9期36卷 161-167页

作者：李金鸣付小雁首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室北京100048

抑郁症以显著而持久的心境低落为主要临床特征,是心境障碍的主要类型,严重影响人们的日常生活和工作。研究人员发现,抑郁症患者与正常人在言语方面存在明显差别。提出一种基于卷积神经网络和长短时期记忆网络的音频抑郁回归模型(DR Audi... 详细信息

抑郁症以显著而持久的心境低落为主要临床特征,是心境障碍的主要类型,严重影响人们的日常生活和工作。研究人员发现,抑郁症患者与正常人在言语方面存在明显差别。提出一种基于卷积神经网络和长短时期记忆网络的音频抑郁回归模型(DR AudioNet)。从特征设计和网络架构两方面进行研究,提出多尺度的音频差分归一化(MADN)特征提取算法。MADN特征描述了非个性化讲话的特性,并根据音频段前后相邻两段的MADN特征设计基于DR AudioNet优化的两个网络模型。实验结果表明,该方法能够有效地识别抑郁程度。

关键词：抑郁症自动诊断语音信号处理深度学习音频特征

来源：评论

学校读者我要写书评

暂无评论

基于UPPAAL的认知机器人控制行为建模与验证

引用

小型微型计算机系统 2016年第6期37卷 1279-1283页

作者：巩卫卫王瑞李晓娟首都师范大学高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室北京100048

随着机器人技术的高速发展,越来越多的人开始聚焦到认知机器人领域的研究,机器人系统中的两大研究领域主要是路径规划和任务规划,而传统的规划问题主要侧重于任务规划.本文的研究是在机器人基于行为的控制结构的基础上,提出机器人系统... 详细信息

随着机器人技术的高速发展,越来越多的人开始聚焦到认知机器人领域的研究,机器人系统中的两大研究领域主要是路径规划和任务规划,而传统的规划问题主要侧重于任务规划.本文的研究是在机器人基于行为的控制结构的基础上,提出机器人系统的任务规划层次框架.认知机器人的大部分的控制行为需要人的参与,这就要求这类机器人系统具有在线自适应的能力,而采用传统的验证方法验证其正确性和实时性上存在一定的局限性.采用形式化方法对认知机器人系统的简单实例建模并验证几个重要的属性,采用时间自动机对系统进行形式化的描述,并结合符号化模型检测工具Uppaal进行验证.针对系统的重要属性采用计算树逻辑的形式表述.

关键词：认知机器人系统行为验证符号化模型检测 Uppaal

来源：评论

学校读者我要写书评

暂无评论

基于精化的可信执行环境内存隔离机制验证

引用

软件学报 2022年第6期33卷 2189-2207页

作者：靳翠珍张倩颖马雨薇李希萌王国辉施智平关永首都师范大学信息工程学院北京100048 高可靠嵌入式系统北京市工程研究中心(首都师范大学) 北京100048 计算机体系结构国家重点实验室(中国科学院计算技术研究所) 北京100190 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学) 北京100048

可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其... 详细信息

可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.

关键词： TEE 内存隔离机制形式化验证精化关系信息流安全性

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：