基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。     

背包问题的最优并行算法

利用分治策略,提出一种基于SIMD共享存储计算机模型的并行背包问题求解算法.算法允许使用O(2^n/4)^1-ε个并行处理机单元,0≤ε≤1,O(2^n/2)个存储单元,在O(2^n/4(2^n/4)^ε)时间内求解n维背包问题,算法的成本为O(2^n/2).将提出的算法与已有文献结论进行对比表明,该算法改进了已有文献的相应结果,是求解背包问题的成本最优并行算法.同时还指出了相关文献主要结论的错误.     

一种基于算法骨架的函数式程序变换技术

如何提高函数式程序设计语言在传统冯·诺依曼机器上的执行速度.及效率,一直是该领域中研究的主要论题,对此,并行图归约技术、并行闭包归约、并行编译、并行程序转换等等技术相继成为改善这种状况的措施。     

基于并行MLFMA最细层数据建立算法的Petri网建模方法

为解决并行多层快速多极子算法(MLFMA)的功能和性能评测的问题,分析了MLFMA算法的关键问题分布树最细层数据的建立,提出了一种可以同时进行性能分析和正确性验证的形式化方法Petri网.将Petri网理论应用到具体的项目中,针对基于消息传递机制的最细层数据建立的并行算法进行形式化建模.在体现Petri网对基于消息传递机制的并行程序进行建模的优越性的同时,为后续进一步的程序正确性验证和性能分析打下基础.     

虫孔路由Mesh上的连通分量算法及其应用

用倍增技术在带有Wormhole路由技术的n×n二维网孔机器上提出了时间复杂度为O(log²n)的连通分量和传递闭包并行算法,并在此基础上提出了一个时间复杂度为O(log³n)的最小生成树并行算法.这些都改进了Store-and-Forward路由技术下的时间复杂度下界O(n).同其他运行在非总线连接分布式存储并行计算机上的算法相比,此连通分量和传递闭包算法的时间复杂度是最优的.     

决策树算法的程序演化方法优化

为了从另一个角度提高决策树算法的效率,对标准的ID3决策树算法进行函数式语言Haskell描述,研究了程序演化策略,推衍出了一个高效等价算法。实验结果证明演化过程是正确的。     

改进NSCT和IHS变换相结合的遥感影像融合

目的 目的为了增强多光谱和全色影像融合质量,提出基于脉冲耦合神经网络（PCNN）的非下采样Contoulet变换（NSCT）和IHS变换相结合的融合方法。方法 先对多光谱图像进行IHS变换提取亮度I分量,采用主成分分析增强I分量得到新的I⁺分量;然后通过NSCT变换分别对I⁺分量和全色图像进行分解,并采用边缘梯度信息激励的PCNN得到融合图像的低频和高频分量;最后进行NSCT逆变换、IHS逆变换得到融合图像。结果 利用资源一号02C卫星数据进行实验,结果表明该算法在保留光谱信息的同时提高了图像空间分辨率,获得了较好的融合效果。结论 结合NSCT和IHS变换的融合方法在视觉效果和客观评价指标上都优于常用的图像融合方法。     

一种基于域知识的协议状态机主动推断算法

现有基于L*算法的协议状态机主动推断方法忽略了协议特有的域知识,将协议报文抽象为相互独立、无意义的符号,并完全随机地生成测试样本进行状态机等价判定,导致产生大量的无效询问和测试样本,在真实网络环境下推断效率较低。在L⁺M算法的基础上提出了一种基于域知识的协议状态机主动推断算法L⁺N,其改进主要体现在:依据会话样本集提取各报文之间的强顺序约束关系来过滤无效的输出询问,构建会话样本集对应的扩展前缀树接受器(Extended Prefix Tree Accepter,EPTA)对输出询问进行预响应,提出了一种基于正例样本变异的等价询问近似判定算法以提升寻找反例的效率。实验结果表明,L⁺N算法能够大幅提高推断效率,并且具有与L⁺M算法相同的推断准确度。     

基于MPI的二维稳态温度场的并行计算

作为颗粒离散元软件并行化的前期研究,对二维稳态导热问题的有限差分法求解程序进行了并行化处理.并行算法将计算域划分为若干个子域,并将各子域上的迭代计算任务分配给相应的处理器执行.同时,算法考虑负载平衡,并采用计算和通信的重叠技术,提高并行算法的效率.通过对二维稳态温度场导热问题的串/并行程序在曙光TC2600刀片服务器上的计算结果进行比较分析,验证了该并行方法的有效性.实验结果表明,计算耗时与通信耗时的比值越大,并行效率越高.     

Radl算法到Apla程序的生成系统

算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率.     

基于IPT硬件的内核模块ROP透明保护机制

Return-Oriented Programming（ROP）是一种流行的利用缓冲区溢出漏洞进行软件攻击的方法,它通过覆写程序栈上的返回地址,使程序在之后执行返回指令时,跳转到攻击者指定位置的代码,因而违反了程序原本期望的控制流.控制流完整性（Control-flow Integrity,简称CFI）检查是目前最流行的ROP防御机制,它将每条控制流跳转指令的合法目标限制在一个合法目标地址集合内,从而阻止攻击者恶意改变程序的控制流.现有的CFI机制大多用于保护用户态程序,然而当前已经有诸多针对内核态的攻击被曝出,其中Return-oriented rootkits^[1] （ROR）就是在有漏洞的内核模块中进行ROP攻击,达到执行内核任意代码的目的.相较于传统的基于用户空间的ROP攻击,ROR攻击更加危险.根据Linux CVE的数据统计,在2014-2016年中,操作系统内核内部的漏洞有76%出现在内核模块中,其中基本上所有被公布出来的攻击都发生在内核模块.由此可见,内核模块作为针对内核攻击的高发区,非常危险.另一方面,当前鲜有针对操作系统内核的CFI保护方案,而已有的相关系统都依赖于对内核的重新编译,这在很大程度上影响了它们的应用场景.针对这些问题,本文首次提出利用Intel Processor Trace （IPT）硬件机制,并结合虚拟化技术,对内核模块进行透明且有效的保护,从而防御针对其的ROP攻击.实验表明该系统具有极强的保护精确性、兼容性和高效性.     

半监督单样本深度行人重识别方法

本文提出一种采用单样本训练的行人重识别方法,在迭代的过程中采用一种渐进学习框架,充分利用有标签数据和无标签数据的特性来优化模型.本文方法主要分为以下3个步骤:(1)训练卷积神经网络来不断优化模型;(2)样本评估:通过本文提出的抽样策略,使用多个模型共同训练,共同挑选出较优的伪标签数据;(3)进行下一轮的训练更新数据.在训练的过程中,我们训练数据由有标签数据、伪标签数据,映射标签数据三部分组成,使用三组数据进行联合学习,每组数据对应使用相应的损失函数对模型进行优化,并且随着迭代的进行,伪标签数据和映射标签数据总是不断更新.在使用单样本训练条件下, rank-1=65.3, mAP=45.6.当训练数据的标注率提升至40%时,rank-1=83.8, mAP=64.9.实验结果表明:本文提出的半监督行人重识别方法可以在使用更少标签数据的情况下,提供与完全监督学习方法相媲美的结果,充分体现了本方法的有效性.     

基于分片复用的多版本容器镜像加载方法

容器将应用和支持软件、库文件等封装为镜像，通过发布新版本镜像实现应用升级，导致不同版本之间存在大量相同数据.镜像加载消耗大量时间，使容器启动时间从毫秒级延迟为秒级甚至是分钟级.复用不同版本之间的相同数据，有利于减少容器加载时间.当前，容器镜像采用继承和分层加载机制，有效实现了支持软件、库文件等数据的复用，但对于应用内部数据还没有一种可靠的复用机制.提出一种基于分片复用的多版本容器镜像加载方法，通过复用不同版本镜像之间的相同数据，提升镜像加载效率.方法的核心思想是：利用边界匹配数据块切分方法将容器镜像切分为细粒度数据块，将数据块哈希值作为唯一标识指纹，借助B-树搜索重复指纹判断重复数据块，减少数据传输.实验结果表明，该方法可以提高5.8X以上容器镜像加载速度.     

一种基于混沌过程神经元水下机器人运动控制方法

由于系统的强非线性以及不确定性，同时考虑到港湾环境下水声信号的噪声大，水下机器人进行精确作业时的运动控制一直是其实用化过程中困挠人们的问题。过程神经网络是传统神经网络的拓展，它增加了一个对于时间的聚合算子，使网络同时具有时空二维信息处理能力，从而更好地模拟了生物神经元的信息处理机制。水下机器人运动控制系统的输入、输出均是随时间连续变化的过程量。在基本神经元模型上，结合S函数和预先规划思想，建立水下机器人过程神经元运动控制模型，参数学习过程中，将遍历性的渐变混沌噪声引入其中，增强控制器全局优化能力。仿真试验表明，该新型控制模型，对于水下机器人的运动非线性控制器具有设计简单、响应速度快、超调小、鲁棒性好等各种优点。     

基于元伪标签和光照不变特征的人脸反欺诈算法

人脸反欺诈(Face anti-spoofing,FAS)在防止人脸识别系统遭受欺诈攻击方面起着至关重要的作用,得益于深度学习网络强大的特征提取能力,基于深度学习的FAS算法取得比基于传统手工特征算法更好的性能,成为近期的研究热点。尽管大多数基于深度学习的FAS算法能在库内达到很好的检测效果,但是跨库检测性能欠佳,主要原因是库内和库外数据往往在不同条件下采集,例如拍摄设备、环境光照和攻击呈现设备不同,导致库内和库外数据的分布不同,两者之间存在域位移。当训练数据的多样性不足时,容易在库内学习过程中过拟合,跨库泛化性能不好。尽管我们可以判断起因,然而在真实世界的应用过程中解决上述问题并不容易。一方面,人脸反欺诈模型难以收集所有场景下的有标签训练样本;另一方面,不同应用场景使得同一因素产生不同的影响,例如,不同场景的光照导致域位移,影响了分类模型对本质性欺诈纹理的提取。为此,本文将元伪标签引入人脸反欺诈任务,提出一种基于元伪标签的人脸反欺诈方法。主要贡献包括:第一,提出一种基于图像块的“教师生成伪标签,学生反馈”半监督学习框架,挖掘局部图像的高区分度特征,解决有标签样本不足的问题;第二,基于局部重力模式(Pattern of localgravitational force,PLGF),设计一种带有注意力模块的光照不变特征分支,抑制应用场景中最容易影响特征提取的光照因素;第三,将元学习与半监督学习框架相结合,优化教师生成伪标签的过程,提高算法的跨库检测能力。与现有流行算法相比,在三个公开的测试数据集(包括CASIA、Replay-Attack和MSU)上,所提出方法在库内测试和跨库测试下均有突出的表现,尤其是泛化性能得到显著提高。在样本数量中等时,在不同库中的半总错误率保持最低。     

医学影像计算机辅助检测与诊断系统综述

计算机辅助检测/诊断（Computer-aided Detection/Diagnosis, CAD）能提高诊断准确性,减少假阳性的产生,为医生提供有效的诊断决策支持.本文的主要目的是分析计算机辅助诊断工具的最新发展.文章以CAD研究较多的四大致命性癌症的发病医学部位为主线,按不同的成像技术和病类,对目前CAD在不同医学图像领域的应用进行了较为详尽的综述,从图像数据集、算法和评估方法等方面作多维度梳理.最后分析了医学图像CAD系统研究领域目前存在的问题并对此领域的研究趋势和发展方向进行展望.     

面向分布式机器学习的大消息广播设计

MPI (Message Passing Interface)专为节点密集型大规模计算集群设计,然而,随着MPI+CUDA (Compute Unified Device Architecture)应用程序以及计算节点拥有GPU的计算机集群的出现,类似于MPI的传统通信库已无法满足.而在机器学习领域,也面临着同样的挑战,如Caff以及CNTK (Microsoft CognitiveToolkit)的深度学习框架,由于训练过程中, GPU会缓存庞大的数据量,而大部分机器学习训练的优化算法具有迭代性特点,导致GPU间的通信数据量大,通信频率高,这些已成为限制深度学习训练性能提升的主要因素之一,虽然推出了像NCCL(Nvidia Collective multi-GPU Communication Library)这种解决深度学习通信问题的集合通信库,但也存在不兼容MPI等问题.因此,设计一种更加高效、符合当前新趋势的通信加速机制便显得尤为重要,为解决上述新形势下的挑战,本文提出了两种新型通信广播机制:(1)一种基于MPI_Bcast的管道链PC (Pipelined Chain)通信机制:为GPU缓存提供高效的节点内外通信.(2)一种适用于多GPU集群系统的基于拓扑感知的管道链TA-PC (TopologyAware Pipelined Chain)通信机制:充分利用多GPU节点间的可用PCIe链路.为了验证提出的新型广播设计,分别在三种配置多样化的GPU集群上进行了实验:GPU密集型集群RX1、节点密集型集群RX2、均衡型集群RX3.实验中,将新的设计与MPI+NCCL1 MPI_Bcast进行对比实验,对于节点内通信和节点间的通信,分别取得了14倍和16.6倍左右的性能提升;与NCCL2的对比试验中,小中型消息取得10倍左右的性能提升,大型消息取得与其相当的性能水平,同时TA-PC设计相比于PC设计,在64GPU集群上实现50%左右的性能提升.实验结果充分说明,提出的解决方案在可移植性以及性能方面有较大的优势.     

基于端到端的多任务商标分卡模型

目前商标分卡处理方法是先进行文本检测再进行区域分类, 最后对不同的区域进行拆分组合形成商标分卡. 这种分步式的处理耗时长, 并且因为误差的叠加会导致最终结果准确率下降. 针对这一问题, 本文提出了多任务的网络模型TextCls, 通过设计多任务学习模型来提升商标分卡的检测和分类模块的推理速度和精确率. 该模型包含一个特征提取网络, 以及文本检测和区域分类两个任务分支. 其中, 文本检测分支采用分割网络学习像素分类图, 然后使用像素聚合获得文本框, 像素分类图主要是学习文本像素和背景像素的信息; 区域分类分支对区域特征细分为中文、英文和图形, 着重学习不同类型区域的特征. 两个分支通过共享特征提取网络, 像素信息和区域特征相互促进学习, 最终两个任务的精确率得以提升. 为了弥补商标图像的文本检测数据集的缺失以及验证TextCls的有效性, 本文还收集并标注了一个由2000张商标图像构成的文本检测数据集trademark_text (https://github.com/kongbailongtian/trademark_text), 结果表明: 与最佳的文本检测算法相比, 本文的文本检测分支将精确率由94.44%提升至95.16%, 调和平均值F1 score达92.12%; 区域分类分支的F1 score也由97.09%提升至98.18%.     

欠驱动刚性航天器时间最优轨迹规划设计

应用伪谱法解决欠驱动刚性航天器的时间最优轨迹规划问题.首先建立欠驱动刚性航天器的动力学和运动学模型,对于给定的初末姿态,选取机动时间最短为待优化的性能指标,并考虑到实际控制输入受限,将其转化为优化过程中的不等式约束条件;然后应用Legendre伪谱法,将优化问题离散化为非线性规划问题进行求解.仿真结果表明,应用伪谱法规划得到的欠驱动航天器最优轨迹,能够较好地满足各种约束条件,而且计算精度高、速度快,具有良好的实时性.     

区块链的安全检测模型

区块链^[1]是去中心化交易平台比特币的底层技术.该系统由分布式数据存储、点对点传输、共识机制、加密算法等计算机技术组成,它的安全性受到广泛关注.目前的研究大多使用数学证明的方法分析每个攻击的作用,本文提出了一种新颖的根据区块链的结构来评估和检测安全性的方法.在真实环境下当一个区块连接超过6个区块后,该区块的内容基本无法改变,被认为是稳定状态,分支产生的概率逐渐降低,因此整个系统的状态是无限循环的.该方法通过分析每个结构到达稳定状态的概率来评估系统的安全性,并通过实验分析了攻击力度,攻击状态和实验循环次数之间的关系,验证了该方法的可行性和有效性.