检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

Ptolemy离散事件模型形式化验证方法

软件学报 2021年第6期32卷 1830-1848页

作者：陆芝浩王瑞孔辉关永施智平首都师范大学信息工程学院北京100048 轻型工业机器人与安全验证北京市重点实验室(首都师范大学) 北京100048 华为技术上海研发中心上海201206 电子系统可靠性与数理交叉学科国家国际科技合作示范基地(首都师范大学) 北京100048

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不... 详细信息

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义;其次设计了一组从离散事件模型到时间自动机的映射规则;然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证;最后,以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.

关键词：形式化验证 Ptolemy离散事件模型模型自动转换时间自动机

在线全文

学校读者我要写书评

暂无评论

“数字信号处理”双语教学课程建设

北京大学学报（哲学社会科学版） 2007年第S2期44卷 122-123页

作者：尹霄丽张健明李宁俎云霄周利清北京邮电大学电子工程学院北京100876

本文介绍了"数字信号处理"课程双语教学课程建设和教学实践情况。文中指出,选取合适的教材对于取得良好的教学效果是非常重要的,授课内容应根据教学大纲的要求作适当增删。在文章中我们介绍了我校正在使用的两本英文原版教材以及我们对... 详细信息

本文介绍了"数字信号处理"课程双语教学课程建设和教学实践情况。文中指出,选取合适的教材对于取得良好的教学效果是非常重要的,授课内容应根据教学大纲的要求作适当增删。在文章中我们介绍了我校正在使用的两本英文原版教材以及我们对教学内容的设置。为了保证教学质量,我们制作了大量的电子教案和交互式的教学演示软件。在课程结束后对教学情况进行了问卷调查,反映出大部分学生对目前的双语教学是认可的,教师应根据实际情况合理分配中英文授课比例。最后文章分析了在双语教学中遇到的主要问题和下一步努力的方向,包括师生的外语水平和教材建设等。

关键词：双语教学数字信号处理课程建设

基于小样本学习的3D动态视觉手势个性化交互方法

在线全文

学校读者我要写书评

暂无评论

电子学报 2013年第11期41卷 2230-2236页

作者：武汇岳王建民戴国忠中山大学传播与设计学院广东广州510006 中国科学院软件研究所人机交互与智能信息处理实验室北京100190

传统的动态手势交互技术如隐马尔科夫模型、神经网络和统计分类器等都需要大量的训练样本,建模过程中需要领域专家的干预、对普通用户来说使用起来较为困难,并且它们针对的是特定的手势集合,很难对其进行扩展.本文通过WOZ实验,分析了用... 详细信息

传统的动态手势交互技术如隐马尔科夫模型、神经网络和统计分类器等都需要大量的训练样本,建模过程中需要领域专家的干预、对普通用户来说使用起来较为困难,并且它们针对的是特定的手势集合,很难对其进行扩展.本文通过WOZ实验,分析了用户的行为特征并给出了基于手势的数字电视交互任务模型;提出了3D动态手势状态转移模型,解决了Midas Touch问题;提出了一种基于小样本学习的动态手势识别方法,解决了传统手势识别方法的缺点;构建了个性化手势设计平台,满足了用户的个性化定制需求;实验评估结果验证了本文方法的有效性.

关键词：人机交互视觉手势小样本学习个性化交互

在线全文

学校读者我要写书评

暂无评论

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

软件学报 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 内存隔离机制形式化验证精化关系信息流安全性

在线全文

学校读者我要写书评

暂无评论

脑电可穿戴无线射频发射芯片系统的研究

光电子 2016年第2期6卷 39-46页

作者：孙建辉刘军涛王蜜霞徐声伟蔡新霞中国科学院电子学研究所传感技术联合国家重点实验室(北方基地)北京中国科学院大学北京

针对脑电EEG (electroencephalograph)传感网络近距离无线传输与可穿戴应用的需要,给出了一款无线射频电路控制系统:集成了模拟电路(8通道低噪声脑电放大器与中速SAR-ADC模数转换)、信道编码EEG-DSP加速器、射频发射芯片。在ISM-2.4 GH... 详细信息

针对脑电EEG (electroencephalograph)传感网络近距离无线传输与可穿戴应用的需要,给出了一款无线射频电路控制系统:集成了模拟电路(8通道低噪声脑电放大器与中速SAR-ADC模数转换)、信道编码EEG-DSP加速器、射频发射芯片。在ISM-2.4 GHz波段,射频物理层使用射频直接上变频架构,通过FSK/OOK (on-off-keying)的数据调制方式;重点优化基于PLL的频率综合器(PLL-FS)与可开关的E类功率放大器(PA-E);PLL-FS具有低相位噪声(?119 dBc/Hz@1 MHz)、锁定时间短(28~60 us)、环路特性好的特点;PA优化了输出功率(4~5 dBm)、功率增加效率PAE(25%)、S-参数等。流水EEG-DSP负责整体系统控制、数据缓存、精简无线信道编码以及输出码流调制射频电路。设计利用Cadence Co.的SpecterRF软件、Synopsys Co.的系列数字软件/Caliber软件进行了功能仿真/物理版图验收,设计使用SmicRF180 nm数模混合工艺进行了加工,流片回来的测试结果表明EEG-DSP与射频发射芯片可以满足实际应用。

关键词：脑电EEG 数模混合芯片设计 FSK/OOK 射频直接上变频相位噪声 DSP流水硬件加速器

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

磁悬浮球电容位移检测方法的仿真分析

传感器与微系统 2024年第11期43卷 135-138页

作者：黄兴花国祥李伟伟闫纪源廉欣芸无锡学院自动化学院江苏无锡214105 华北电力大学电气与电子工程学院北京102206 南京信息工程大学自动化学院江苏南京210044

为精确非接触地监测磁悬浮球体的位移,本文设计了两种电容位移检测方案:单端方案和差分方案。运用COMSOL Multiphysics软件,为这两种方案构建了有限元仿真模型,并分析了测试电容值与磁悬浮球位移之间的关系。在单端式方案中,测试电容与... 详细信息

为精确非接触地监测磁悬浮球体的位移,本文设计了两种电容位移检测方案:单端方案和差分方案。运用COMSOL Multiphysics软件,为这两种方案构建了有限元仿真模型,并分析了测试电容值与磁悬浮球位移之间的关系。在单端式方案中,测试电容与悬浮球位置的关系呈现出非线性特征,且这种非线性随球体与电容极板间距离的增加而更加明显。相比之下,差分式方案展现出测试电容与磁悬浮球位移之间的线性关系,但在量程增加时,其测试灵敏度有所下降。得益于电容检测电路技术的不断进步,提出的差分式电容位移检测方案在超过6.4 mm的磁悬浮球位移范围内,有望实现纳米级的位移检测精度。

关键词：磁悬浮电容传感器位移测量有限元分析

同方期刊数据库博看期刊评论

在线全文

学校读者我要写书评

暂无评论

格林定理的形式化及其初步应用

计算机工程与科学 2023年第7期45卷 1178-1187页

作者：刘永梅王国辉关永张景芝施智平董璐首都师范大学信息工程学院北京100048 电子系统可靠性与数理交叉学科国际科技合作基地北京100048

格林定理广泛应用于物理学、流体力学和化学等领域。通常使用传统的计算机仿真和数值计算方法构建基于格林定理的系统模型。然而,由于工具软件可能存在的系统缺陷导致模型出现偏差,从而使任务失败。为解决上述问题,采用基于高阶逻辑的... 详细信息

格林定理广泛应用于物理学、流体力学和化学等领域。通常使用传统的计算机仿真和数值计算方法构建基于格林定理的系统模型。然而,由于工具软件可能存在的系统缺陷导致模型出现偏差,从而使任务失败。为解决上述问题,采用基于高阶逻辑的形式化方法,在定理证明器HOL Light中实现了格林定理相关内容的高阶逻辑建模与验证。首先,对梯度、散度等基本概念和性质进行了形式化描述;其次,对格林定理及其性质进行了形式化建模与验证;最后,基于格林定理的形式化模型完成了地下水控制模型的高阶逻辑推导,进而确保系统模型的安全性。

关键词：形式化验证定理证明格林定理 HOL Light

壳体开孔位置方式对压电振动加速度计屏蔽效能的影响

在线全文

学校读者我要写书评

暂无评论

中南大学学报（自然科学版） 2013年第S1期44卷 425-429页

作者：解连鑫李邓化庞美飒郝翠北京信息科技大学自动化学院北京100101 北京交通大学电子信息工程学院北京100044

由于压电振动加速度计壳体需要开孔穿过电源线和信号传输线等,当存在电磁脉冲干扰时,电磁脉冲会通过孔进入加速度计内部,导致加速度计失效。为此,应设计合理的开孔壳体使加速度计具有高抗电磁干扰性,使用CST软件利用有限积分(FIT)算法... 详细信息

由于压电振动加速度计壳体需要开孔穿过电源线和信号传输线等,当存在电磁脉冲干扰时,电磁脉冲会通过孔进入加速度计内部,导致加速度计失效。为此,应设计合理的开孔壳体使加速度计具有高抗电磁干扰性,使用CST软件利用有限积分(FIT)算法对具有不同位置和排列方式的孔的壳体进行屏蔽效能仿真。通过仿真分析,针对论文中仿真的圆柱形壳体,提出应将孔安置在壳体内壁上、下1/4处并采取开3个尽量小的孔呈三角形排列方式的方案。实现增强加速度计壳体抗电磁脉冲干扰能力的目标,大大减少电磁脉冲对压电振动加速度计的影响。

关键词：加速度计壳体电磁脉冲 FIT算法屏蔽效能

规律性有氧运动对成年人血浆白介素-6水平影响的Meta分析

在线全文

学校读者我要写书评

暂无评论

体育科学 2015年第10期35卷 90-96,F0003页

作者：朱光辉李常青李欣江南大学体育学院江苏无锡214122 北京体育大学研究生院北京100084 成都大学体育学院四川成都610106

目的:评价规律性有氧运动对成年人血浆中IL-6浓度的影响效果。方法:电子检索PubMed、Embase、Web of Science、万方、维普和知网数据库,检索期限均从各个数据库收录起始年限起至2014年12月,全面收集规律性有氧运动影响成人血浆中IL-6浓... 详细信息

目的:评价规律性有氧运动对成年人血浆中IL-6浓度的影响效果。方法:电子检索PubMed、Embase、Web of Science、万方、维普和知网数据库,检索期限均从各个数据库收录起始年限起至2014年12月,全面收集规律性有氧运动影响成人血浆中IL-6浓度的随机对照实验(RCT),Cochrane偏倚风险评估工具评价纳入研究的方法学质量,Stata 13.0软件进行统计分析。结果:共纳入32个RCT,2 768个成年人,其中,慢性炎症性疾病患者670人。纳入研究中较高等级的方法学质量的研究有10个、中等研究质量12个、低等质量10个。Meta分析结果显示,规律性有氧运动可明显降低成年人血浆中IL-6浓度,SMD=-0.42(95%CI:-0.62^-0.18,P=0.001),但异质性较为明显(I2=88.1%)。通过Meta回归分析排除健康状态及其他可能的混杂因素影响后,异质性有所降低(I2=58.34%)。进一步的亚组分析结果提示,规律性有氧运动对健康成年人血浆IL-6浓度的降低效果不明显(SMD=-0.189,95%CI:-0.412~0.035,P=0.098),但对肥胖和炎症相关的慢性病患者的降低效果显著,其SMD(95CI%)分别为-0.593(-1.137^-0.05,P=0.032)和-0.717(-1.324^-0.123,P=0.021)。结论:规律性有氧运动能够有效降低成年人血浆中IL-6浓度,尤其对炎症性慢性病患者效果更为显著,但由于异质性和发表偏倚的影响,结论尚需开展更多高质量的研究加以验证。

关键词：规律性有氧运动成年人 IL-6水平 Meta分析