基于微流控技术的磁流体对外加磁场及温度的太赫兹特性研究

磁流体是将超微磁性粒子均匀地分布在载基液中,形成的胶态液体磁性材料,它打破了传统固体磁性材料的形态,是一种同时具有固体磁性和液体流动性的新型材料,具有非常广泛的应用前景。目前磁流体已经被应用于医学领域,已有研究表明,磁流体可被用于癌细胞的治疗、细胞的分离以及靶向给药等;另外,磁流体还可以应用于密封、润滑等方面。太赫兹波是指频率范围在0.1~10 THz,波长范围在30~3000μm的电磁辐射。由于许多生物分子的振动和转动模式均处于太赫兹波频段,并且太赫兹波的能量较低,不会破坏被测物品,所以太赫兹波可用于无损检测,是一种安全可靠的测量方法。微流控技术可用于对极少量液体样品的测量,具有操作简单、检测速度快、节约被测样品等优点。该研究将太赫兹技术与微流控芯片技术相结合,通过改变外加磁场的时间和温度,研究了磁流体的太赫兹时域谱和频域谱的变化情况,发现在外加不同时间的磁场强度时,随着时间的增加,磁流体的太赫兹时域谱图右移,频域谱图强度下降;外加不同温度时,随着温度的增加,同样出现时域谱图右移,透射强度降低的现象。初步认为磁流体中的磁性粒子在外加磁场下聚集定向排列,随着时间的延长,近似认为纳米粒子团簇半径增大,使得太赫兹波不易透过从而使其强度变低;在温度升高时,分子热运动加剧,分子振动和转动加强,使得太赫兹波不易透过进而强度变低。由于利用太赫兹研究磁流体特性方面的相关报道较少,该研究为探究磁流体提供了新的方法;对外加磁场下的磁流体太赫兹特性的研究可在医学领域的广泛应用,为太赫兹技术在生物医学方面提供了新的途径,为磁流体的深入应用和研究提供了技术支持。

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

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

基于数据冗余性的近似计算技术

为解决神经网络中爆炸式增长的数据量所加剧的计算机系统存储墙问题,针对经典近似方法在平衡精确度和开销问题上的不足,提出一种利用相邻数据之间相似特征以及神经网络中数据冗余性的优化方法。通过分析数据密集型应用的数据特征,提出针对权值的稀疏矩阵压缩,针对输入数据的重复值压缩和相邻小范围浮动数据近似的方案,设计神经网络拓扑感知的冗余数据近似方法,在合理范围内实现数据近似。实验结果表明,相比于SNNAP方案输出质量平均提高了8.16%,压缩率达到51.38%,为提高数据密集型应用的系统加速比提供了可行性。

基于微流控技术的磁流体载基液的太赫兹透射特性研究

太赫兹(THz)是指频率在0.1~10 THz的电磁波,其波长在30~3000μm范围内。由于自然界许多小分子的振动、转动等的频率均在太赫兹波段,并且太赫兹的低电子能特性使其在实验过程中不会对待测样品造成破坏,所以太赫兹技术被广泛地应用于无损检测、生物医学等领域。但是太赫兹在铁磁领域的相关报道还是较少的,因此本研究利用太赫兹时域光谱系统研究了一种新型磁性材料:磁流体的组成部分-载基液的太赫兹透射特性。磁流体是一种兼具液体流动性和固体磁性的新型功能材料,其打破了传统磁性材料的固体形态。磁流体由Fe_(3)O_(4)纳米级颗粒以及载基液构成。在前人的研究成果中发现磁性液体不仅具有良好的磁光效应,而且对于一定频率的太赫兹波具有高透射率;另外,在极低频电磁场作用下其可用于医学上的肿瘤治疗,可作为靶向治疗的载药系统。由于磁流体的组成部分-载基液成本较高,因此在实验中运用了微流控技术。微流控技术对检测样品的消耗少、检测速度快,并且可以根据实验需求自行设计沟道,因此是一种便捷的、灵活性好的检测方式。采用对太赫兹波具有高透过率的石英材料制成了夹心式的太赫兹微流控芯片。首先将两块3 cm×3 cm×2 mm的石英玻璃作为基片和盖片,再把强粘黏性双面胶剪刻成镂空样式,形成2 cm×2 cm的方形区域,然后把盖片和基片通过雕刻好的强粘黏性双面胶键合,其沟道厚度为50μm,可以用于对少量液体的探测,并且可以使载基液呈薄膜状。之后将太赫兹技术和微流控技术相结合,利用太赫兹时域光谱(THz-TDS)系统研究了载基液的太赫兹透射特性,通过对太赫兹时域光谱以及频域光谱的研究发现,装有载基液的微流控芯片的信号强度高于空的微流控芯片,这一发现为载基液的应用和深入研究提供了技术支持。

基于微流控技术的水的太赫兹吸收特性研究

很多生物大分子的特征振动模式和转动模式都位于太赫兹波段范围内,且太赫兹波的低电子能特性使其在实验过程中不会对待测样品造成破坏,所以可以采用太赫兹技术来鉴别生物样品。在许多研究中,生物样品都是溶液状态,溶液中水和其他分子之间的相互作用涉及很多生物现象,所以研究水的太赫兹特性就显得至关重要。众所周知,水分子是十分常见的极性分子,分子间氢键会与太赫兹波发生强烈的相互作用,从而使得水对太赫兹波有很强的吸收作用,导致利用太赫兹技术研究水溶液中生物样品的动态特性变得相当困难。为了解决这一难题,可以引入微流控技术。微流控技术以能精确操控微尺度流体而著称,其沟道深度可以达到50μm甚至更小。由于微流控技术减小了太赫兹波在流体中的传播距离,从而极大地减小了水对太赫兹波的吸收。本研究采用对太赫兹波具有高透过率的Zeonor 1420R材料制成了夹心式微流控芯片,芯片上微沟道的长度、宽度和深度分别为3 cm,4 mm和50μm,太赫兹探测区的直径为3 mm。在制作微流控芯片时,利用厚度为50μm的强黏性双面胶代替传统夹心式微流控芯片中的聚二甲基硅氧烷(PDMS)薄膜,使微流控芯片在加热过程中不再有漏液现象。另外,设计了一个温控系统,它由加热片、温度传感器和温控仪构成,该温控系统能够以0.1℃的精度控制温度。利用该系统对微流控芯片中的去离子水进行加热,从20~90℃每隔5℃进行一次太赫兹透射测量,通过对实验数据的分析,发现随着温度升高,水的太赫兹透过率不断减小,说明水对太赫兹波的吸收随着温度的升高而变大。此结果为未来在不同环境温度下利用微流控技术研究液态样品的太赫兹吸收特性提供了先决条件,为未来太赫兹的应用与发展提供技术支持。

体系结构特征参数指导的近似计算技术

能耗是制约微处理器发展的瓶颈之一,近似计算技术能够放松对精度的要求提高能效性.不同的应用程序对精度的需求各不相同,但现有技术选择近似程度时没有考虑程序需求,因而无法保证达到最优的能效性.针对上述问题本文提出了体系结构特征参数指导的近似计算技术,建立了体系结构参数同近似敏感度之间的联系,通过机器学习方法选择对近似影响较大的参数,利用分类决策树建立区分程序近似敏感度的分析模型,并基于分析结果指导近似程度的选择.实验结果显示,本文的方法能够为不同程序选择合适的近似程度,实现计算精度和能效性的折中优化.

微分相位衬度计算机层析成像的感兴趣区域重建方法

基于光栅干涉仪系统的X射线微分相位衬度计算机层析成像,不仅可以重建物体的线性衰减系数,还可以重建物体的相移系数和线性散射系数.在实际应用时,大面积光栅不易获得,常常遇到样品大于光栅的情况.当用小于样品的光栅对样品进行扫描时,样品超出光栅成像视野的部分会导致微分相位投影信息被截断.本文针对微分相位衬度计算机层析成像提出了一种相移系数的感兴趣区域重建方法.该方法利用物体相移系数和线性衰减系数(即折射率实部减小量和折射率虚部)之间的近似线性关系;通过重建相移系数的Lambda函数和线性衰减系数的Lambda逆函数的多项式组合,近似重建物体感兴趣区域的相移系数.数值模拟实验依据菲涅耳衍射积分理论,进行计算机仿真X射线的传播过程和光栅成像过程.实际实验利用上海同步辐射BL13W1站的Talbot光栅干涉仪系统,分别对标准模体和生物样品进行光栅微分相位衬度计算机层析成像.数值模拟和实际实验结果都验证了该方法的有效性.

太赫兹光场成像的实验与处理研究

太赫兹波的频率介于红外线与微波之间,其独特优势使得太赫兹三维成像已成为国内外的研究热点。为了将光场成像技术拓展到太赫兹波段,介绍了太赫兹光场成像的实验与处理方法。采用太赫兹相机阵列采集到了一系列特定视角的太赫兹光场数据。针对由成像系统的器件限制导致图像存在较强噪点等问题,通过离散余弦变换(Discrete Cosine Transform,DCT)滤波达到了较好的去噪效果并有效保留了图像的细节信息。利用峰值信噪比(Peak Signal-to-Noise Ratio,PSNR)和结构相似性(Structural SIMilarity,SSIM)图像质量评价指标对比了多种滤波去噪方法,证明了DCT滤波方法对于太赫兹图像预处理的可行性。通过选取不同深度值得到了不同景深处的图像重构结果,初步实现了太赫兹光场成像的数字重聚焦。

太赫兹光场成像的深度估计方法与实验研究

在前期工作中,通过对太赫兹光场图像进行离散余弦变换(Discrete Cosine Transform,DCT)滤波和数字重聚焦,初步实现了图像去噪和前后景分割。为了进一步得到质量更高的太赫兹光场原数据并达到更加精确的深度分割效果,改进了实验方案及处理方法,并提出了一种基于极平面图像(Epipolar Plane Image,EPI)的太赫兹光场深度估计方法。在太赫兹图像特性的基础上,给出了深度与视差的关系,并利用局部视差和置信度构建了全局深度图,从而达到了深度估计的目的。最后,在实验中通过10×10的相机阵列采集太赫兹光场数据,得到了准确聚焦于不同平面的重聚焦结果和高分辨度的深度估计图,实现了太赫兹光场成像的深度估计。

可信执行环境软件侧信道攻击研究综述

为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(TEE)技术,通过对硬件和软件进行隔离为安全敏感程序提供一个与通用计算环境隔离的安全运行环境.侧信道攻击从传统的需要昂贵设备发展到现在仅基于微体系结构状态就能通过软件方式获取机密信息的访问模式,从而进一步推测出机密信息.TEE架构仅提供隔离机制,无法抵抗这类新出现的软件侧信道攻击.深入调研了ARM TrustZone、Intel SGX和AMD SEV这3种TEE架构的软件侧信道攻击及相应防御措施,并探讨其攻击和防御机制的发展趋势.首先,介绍了ARM TrustZone、Intel SGX和AMD SEV的基本原理,并详细阐述了软件侧信道攻击的定义以及缓存侧信道攻击的分类、方法和步骤;之后从处理器指令执行的角度,提出一种TEE攻击面分类方法,利用该方法对TEE软件侧信道攻击进行分类,并阐述了软件侧信道攻击与其他攻击相结合的组合攻击;然后详细讨论TEE软件侧信道攻击的威胁模型;最后全面总结业界对TEE软件侧信道攻击的防御措施,并从攻击和防御两方面探讨TEE软件侧信道攻击未来的研究趋势.

基于微流控芯片的钾盐溶液太赫兹光谱特性研究

许多生物分子的振动及转动能级都在太赫兹波段,因此太赫兹时域光谱技术可以用来探测生物分子。并且由于太赫兹波的光子能量较低,仅为毫电子伏量级,在探测过程中不会破坏生物样品,所以太赫兹时域光谱技术在未来生化检测等研究领域具有非常广泛的应用前景。研究表明,大多数生物分子需要在液体环境中才能充分发挥其生物活性,然而水溶液中的氢键在太赫兹波段会产生强烈的吸收。另外,水分子是极性分子,太赫兹波对极性分子也有很强的共振吸收,这使得利用太赫兹时域光谱技术检测液体环境中的活性生物分子非常困难。因此,许多研究团队将太赫兹时域光谱技术与微流控技术相结合,以减少各种因素对生物分子检测的影响。微流控技术是通过减小微流控芯片中液体池的深度来减少液体样品与太赫兹波的作用距离,从而减少水溶液对太赫兹波的吸收。使用对太赫兹波的透过率高达95%的环烯烃共聚物(COC:Zeonor 1420R)为材料制作了双层微流控芯片,该微流控芯片内部液体池的长度和宽度均为4 cm,深度为50μm。此外,由于在电解质溶液中存在大量自由移动的阴阳离子,所以为了探究电解质溶液中自由移动的阴阳离子对太赫兹透射特性的影响,使用外加电场装置对注入液体样品的微流控芯片施加电压。该外加电场装置包括电源,一个封装在有机玻璃盒中的ZVS电路和一个输出电压为10000 V的直流高压包。在此基础上研究了五种相同浓度的钾盐溶液以及这五种钾盐溶液在外加不同时间的恒定电场中的太赫兹波的透射特性,为进一步加强THz技术在生物化学中的应用提供了依据。再者,电解质溶液中的大量阴阳离子在外加电场的作用下会发生运动,这为利用太赫兹时域光谱技术研究电解质溶液的动态特性提供了技术支持。

TrustZone中断隔离机制的形式化验证

TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断被通用执行环境处理,从而影响可信执行环境的安全性.本文提出ARMv8 TrustZone架构中断隔离机制的形式化验证方法,在定理证明器Isabelle/HOL中建立包含中断隔离机制关键软硬件的形式化模型,该模型为状态迁移系统,包括中断处理程序、TrustZone Monitor、中断控制器等组件;在证明模型满足正确性的基础上,通过展开定理验证无干扰、无泄露、无影响等信息流安全属性,结果表明TrustZone中断隔离机制满足信息流安全属性,在中断处理过程中不存在隐蔽的信息流通道.

基于对抗生成网络的太赫兹安检图像分割算法

为解决太赫兹成像分辨力低,危险品边缘模糊,无法有效对危险品进行分割的问题,提出一种基于对抗式生成网络与多头注意力机制的新型网络架构,并用于太赫兹安检图像智能分割。通过学习深层鉴别器的特征图优化生成器,获得更加真实的生成图像;引入多头注意力机制提升模型对危险品特征的识别能力。分割太赫兹安检图像的大量实验结果表明,相较于传统卷积神经网络,提出的对抗生成网络在相同深度下具有更好的泛化能力;多头注意力机制的引入强化了模型对危险品特征的学习,在未知危险品类别的情况下同样拥有较好的效果,其交并比(IOU)指标相较ResNet-50提高9.6%,相较ResNet-18提高21.3%,相较U-Net提高12.3%。本文研究有利于图像分割算法更准确、高效地处理太赫兹安检图像,有助于拓宽太赫兹智能安检系统的进一步应用。

基于多尺度细节增强的面部表情识别方法

人类面部表情是其心理情绪变化的最直观刻画,不同人的面部表情具有很大差异,现有表情识别方法均利用面部统计特征区分不同表情,其缺乏对于人脸细节信息的深度挖掘。根据心理学家对面部行为编码的定义可以看出,人脸的局部细节信息决定了其表情意义。因此该文提出一种基于多尺度细节增强的面部表情识别方法,针对面部表情受图像细节影响较大的特点,提出利用高斯金字塔提取图像细节信息,并对图像进行细节增强,从而强化人脸表情信息。针对面部表情的局部性特点,提出利用层次结构的局部梯度特征计算方法,描述面部特征点局部形状特征。最后,使用支持向量机(SVM)对面部表情进行分类。该文在CK+表情数据库中的实验结果表明,该方法不仅验证了图像细节对面部表情识别过程的重要作用,而且在小规模训练数据下也能够得到非常好的识别结果,表情平均识别率达到98.19%。

基于网络演算的动态可重构总线建模及关键参数确定

嵌入式系统在使用UM-BUS总线时,总线仲裁时隙大小、协议包大小等关键参数对总线性能有很大的影响;必须通过数学模型建立与仿真分析等手段确定总线关键参数,确保总线传输时延满足系统的实时性需求.本文针对UM-BUS总线的实时性进行了建模和分析,利用网络演算理论建立了总线系统数据服务模型,得出了数据传输时延上界的解析结果表达式.给出了一个典型的无人艇控制系统实例,确定了最优的关键参数设置.通过仿真分析结果与实验统计结果的对比,验证了模型的准确性.

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

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

基于Spark的大数据访存行为跨层分析工具

大数据时代的到来为信息处理带来了新的挑战,内存计算方式的Spark显著提高了数据处理的性能.Spark的性能优化和分析可以在应用层、系统层和硬件层开展,然而现有工作都只局限在某一层,使得Spark语义与底层动作脱离,如操作系统参数对Spark应用层的性能影响的缺失将使得大量灵活的操作系统配置参数无法发挥作用.针对上述问题,设计了Spark存储系统分析工具SMTT,打通了Spark层、JVM层和OS层,建立了上层应用程序的语义与底层物理内存信息的联系.SMTT针对Spark内存特点,分别设计了针对执行内存和存储内存的追踪方式.基于SMTT工具完成了对Spark迭代计算过程内存使用,以及跨越Spark,JVM和OS层的执行存储内存使用过程的分析,并以RDD为例通过SMTT分析了单节点和多节点情况下Spark中读和写操作比例,结果表明该工作为Spark内存系统的性能分析和优化提供了有力的支持.

面向数据流的ROS2数据分发服务形式建模与分析

机器人操作系统(robot operating system,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题,ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法,分析、验证ROS2系统数据分发机制的实时性和可靠性.首先,提出一种面向数据流的ROS2数据分发服务的形式化验证框架,并对通信系统模块建立概率时间自动机模型;其次,运用概率模型检测器,通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性;最后,基于重传机制、服务质量(quality of service,简称QoS)策略分析,通过设置和调整服务质量参数,实现不同的数据需求和传输方式的量化性能分析,为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考.

多纹理分级融合的织物缺陷检测算法

针对织物缺陷检测过程中纹理分布的复杂多样性引起误检和漏检的问题,结合织物纹理周期性特点,提出一种多纹理分级融合的织物缺陷检测算法。在检测过程中,首先利用织物缺陷图像的Tamura粗糙度图,对缺陷区域进行初步定位和自适应性生长,将初步定位的区域映射到原始织物图像中;其次根据织物图像的周期性分布特征,对初步定位区域进行分块,提取图像块的局部相位量化(LPQ)特征、Tamura特征,并将2种特征融合;然后计算融合特征与正常块特征的相似度,获取相似度图;最后将初步定位区域的经纬向特征图与相似度特征图融合,检测缺陷存在的区域。经TILDA织物纹理库数据的实验测试结果表明,缺陷区域的初步定位和自适应生长,降低了缺陷检测过程的冗余度,提高了检测效率,避免了织物缺陷检测过程中的误检和漏检情况。

太赫兹光场数据采集与数字重聚焦实验研究

本文对太赫兹光场数据采集与数字重聚焦成像进行实验研究。太赫兹成像因其穿透性、无损性等优点,近年来备受国内外研究者关注。太赫兹波段的光场成像技术有望增强图像质量、改善应用效果。本文在分析光场成像基本原理、系统结构、重建方法的基础上,应用太赫兹焦平面阵列相机进行太赫兹光场数据采集和数字重聚焦实验。首先采集太赫兹光场原始数据,然后通过数字重聚焦进行计算成像,最后对重构图像做增强处理,得到了深度、角度及目标物轮廓分辨力强的太赫兹图像。实验证明了太赫兹光场成像技术的可行性及其改善图像质量、丰富复现效果的能力。