摘要:

摘要:设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现，侧重于从高可信性角度进行语言设计，包括形式化定义该语言的类型系统和操作语义，以及设计其可信编译结构.基于对可重构硬件基本需求的充分理解，从软硬件协同角度出发，最终明确了P3语言的核心特性及其编译器P3C的可信编译结构.由于可重构数据包解析器是软件定义网络（SDN）、可编程数据平面的重要一环，因此，实现P3C的可信编译结构将对SDN的安全性具有重大意义.期待P3C项目的开展能够促进网络与形式化领域相关工作的进一步研究.

摘要:随着应用软件体系结构风格变化和规模变大，其运行环境变得日趋复杂，对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计关于需求满足性验证在建模与验证中需要多种工具的支持.应用系统体系结构在设计阶段的需求满足验证，有助于客观评价应用系统部署方案和系统如期上线以及主动运维.面向应用系统体系结构设计及其验证，在模型驱动的软件工程背景下提出一种高阶类型化可验证应用系统体系结构建模语言（V_ASAML）与可验证应用系统体系结构建模方法（V_ASAMM）.V_ASAML语言通过定义类型和项的语法和语义，描述构成应用系统体系结构的类型和对象的结构，通过定义两种类型规则及其类型检查算法，判定Γ|-t：T和Γ|-R（T₁，T₂）是否成立，其中，结构类类型规则用于描述应用系统体系结构中的组成部分，关系类类型规则用于描述组成部分之间的关系和配置.V_ASAMM方法给出了应用系统体系结构建模过程，包括构建M_bd（基本数据类型）、M_bti（基本接口类型）、M_dev（设备类型）和M_frwk（应用系统框架）这4层，以及自动生成层内与层间类型之间关系对应的类型规则，同时定义了设备类型服务调用图（G_DSI）用以刻画部署要求，定义了类型序列及其正确性用以刻画需求期望性质，并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统V_ASAMS，其中，建模编辑环境支持应用系统部署方案的设计过程，验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.

摘要:PaxosStore是腾讯开发的高可用分布式存储系统，现已用于全面支持微信核心业务.PaxosStore实现了分布式共识协议Paxos的一种变体，称为TPaxos.TPaxos的新颖之处在于其“统一性”：为每个参与者维护统一的状态类型，并采用统一格式的消息进行通信.然而，这种设计方案也带来了TPaxos与Paxos之间的诸多差异，给理解TPaxos造成了障碍.其次，虽然腾讯开源了TPaxos协议的核心代码（包括伪代码与C++代码），但TPaxos仍缺少抽象而精确的形式化规约.最后，根据文献检索，TPaxos的正确性尚未经过必要的数学论证或者形式化工具的检验.针对这些情况，有3个主要贡献：首先，从经典的Paxos协议出发，论证如何逐步推导出TPaxos协议.基于这种推导，可以将TPaxos看作Paxos的一种自然变体，更易于理解.其次，给出了TPaxos协议的TLA+形式化规约.在开发规约的时候发现，TPaxos协议描述中存在至关重要但并未充分阐明的微妙之处：在消息处理阶段，参与者（作为接受者角色）是先作出“不再接受具有更小编号的提议”的承诺（promise），还是先接受（accept）提议?这导致了对TPaxos的两种不同理解，并促使提出TPaxos的一种变体，称为TPaxosAP.在TPaxosAP中，参与者先接受提议后作承诺.最后，使用精化（refinement）技术论证了TPaxos与TPaxosAP的正确性.特别地，由于已知的投票机制Voting不能完全描述TPaxosAP的行为，首先提出了适用于TPaxosAP的投票机制EagerVoting，然后建立了从TPaxosAP到EagerVoting以及从EagerVoting到Consensus的精化关系，并使用TLC模型检验工具验证了它们的正确性.

摘要:Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用，比如区块链系统以及谷歌文件系统等，其安全性证明越来越重要.在定理证明工具Coq中，形式化描述和定义了Lamport的Basic Paxos算法，并且证明了其满足共识性.

摘要:为确保星上操作系统中任务管理设计的可靠性，利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度，基于星上操作系统任务管理的基本机制，提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行形式化建模，并在Coq中实现.针对建立的需求层模型，提出6条与实际星上操作系统任务管理一致的性质并进行验证.给出其中一条性质在Coq中的验证过程，结果表明，模型满足该条性质.

摘要:基本并行进程是一个用于描述和分析并发程序的模型，是Petri网的一个重要子类.EG逻辑是一种在Hennessy-Milner Logic的基础上增加EG算子的分支时间逻辑，其中的AF算子表示从当前的状态出发性质最终会被满足，因此EG逻辑是能够表达活性的逻辑.然而，基于基本并行进程的EG逻辑的模型检测问题是不可判定的.由此，提出了基本并行进程上EG逻辑的限界模型检测方法.首先给出了基本并行进程上EG逻辑的限界语义，然后采用基于约束的方法，将基本并行进程上EG逻辑的限界模型检测问题转化为线性整数算术公式的可满足性问题，最后利用SMT求解器进行求解.

摘要:软件系统自适应提供了应对动态变化的环境和不确定的需求的技术方案.在已有的软件系统自适应性的相关研究中，有一类工作将软件系统自适应性转换为回归、分类、聚类、决策等问题，并利用强化学习、神经网络/深度学习、贝叶斯决策理论和概率图模型、规则学习等机器学习算法进行问题建模与求解，并以此构造软件系统自适应机制.将其称为机器学习赋能的软件自适应性.通过系统化的文献调研，综述了该研究方向的前沿工作：首先介绍基本概念，然后分别从机器学习、软件自适应的视角对当前工作进行分类；按机器学习算法、软件对外交互、软件对内控制、自适应过程、自适应任务和学习能力的对应关系等方面进行分析；最后对未来的研究进行展望.

摘要:缺陷定位是软件工程研究最活跃的领域之一.大部分软件缺陷都会被提交到类似于Bugzilla和Jira的缺陷追踪系统中.由于提交的缺陷报告数量过多，开发人员不能及时处理，因而迫切需要一个自动化工具来帮助开发人员识别缺陷相关源代码文件.研究人员已提出了大量缺陷定位技术.基于信息检索的软件缺陷定位技术（information retrieval-based bug localization，简称IRBL）利用了缺陷报告的文本特性，并且由于计算成本低、对不同的程序语言更具普适性而成为缺陷定位领域的研究热点，取得了一系列研究成果.然而，IRBL技术也在数据预处理、相似度计算和工程应用等方面存在诸多挑战.鉴于此，对现有的IRBL技术进行梳理总结，主要内容包括：（1）梳理了IRBL中数据预处理的过程和信息检索通用方法；（2）对IRBL技术中利用的数据特征进行了详细的分类和总结；（3）总结了技术评估中使用的性能评估指标；（4）归纳出了IRBL技术的关键问题；（5）展望了IRBL技术的未来发展.

摘要:代数次数作为布尔函数重要的密码学指标，在密码算法的设计与分析中有着重要的应用.主要研究布尔函数代数次数的求解及其在分组密码SIMON-like算法中的应用.首先，在利用真值表求解代数正规型算法的基础上建立了基于CUDA的并行求解架构，协同利用CPU和GPU的计算资源，极大地缩短了求解代数次数的时间，在较短的时间内求解了SIMON32算法和SIMECK32算法任意轮数的代数正规型和代数次数；其次，在Cube攻击理论的基础上，根据代数次数和超多项式取值之间的关系，设计了估计代数次数的概率算法，估计了一般SIMON-like算法布尔函数的代数次数；最后，从布尔函数代数次数的角度出发，给出了SIMON-like算法在选择不同循环移位参数表现的差异性，进而给出循环移位参数的选取依据.实验结果表明，SIMON算法在原始参数下，达到最大代数次数所需的轮数最短，原始参数具有更高的安全性.

摘要:情感识别是多学科交叉的研究方向，涉及认知科学、心理学、信号处理、模式识别、人工智能等领域的研究热点，目的是使机器理解人类情感状态，进而实现自然人机交互.首先，从心理学及认知学角度介绍了语音情感认知的研究进展，详细介绍了情感的认知理论、维度理论、脑机制以及基于情感理论的计算模型，旨在为语音情感识别提供科学的情感理论模型；然后，从人工智能的角度，系统地总结了目前维度情感识别的研究现状和发展，包括语音维度情感数据库、特征提取、识别算法等技术要点；最后，分析了维度情感识别技术目前面临的挑战以及可能的解决思路，对未来研究方向进行了展望.

摘要:情感分析旨在判断文本的情感倾向，而评论质量检测旨在判断评论的质量.情感分析和评论质量检测是情感分析中两个关键的任务，这两个任务受多种因素的影响而密切相关，同一个产品的情感倾向具有相似的情感极性；同时，同一个用户发表的评论质量也具有一定的相似性.因此，为了更好地研究情感分类和评论质量检测任务的相关性以及用户信息和产品信息分别对情感分类和评论质量检测的影响，提出了一个情感分析和评论质量检测联合模型.首先，使用深度学习方法学习评论的文本信息作为联系两个任务的基础；然后，将用户评论及产品评论作为用户的表示和产品的表示；在此基础上，采用用户注意力机制对用户的表示进行编码，采用产品注意力机制对产品的表示进行编码；最后，将用户表示和产品表示结合起来进行情感分析和评论质量检测.通过在Yelp2013和Yelp2015数据集上的实验结果表明，该模型与现有的神经网络模型相比，能够有效地提高情感分析和在线评论质量检测的性能.

摘要:随着Android设备的流行和普及，Android生态系统的碎片化问题越发严重.为了确保应用质量，Android应用需要在多种设备上进行测试.为了应对大量重复机械的测试工作，学术界和工业界提出了众多跨设备的测试方法，但目前的方法还有较多的局限性：（1）手工编写设备无关的测试脚本耗时且容易出错；（2）现有录制/重放方法生成的测试脚本在跨设备重放时会出现各种问题，导致重放失败；（3）由于缺少足够的Android设备，应用难以在大量不同类型的设备上进行测试；（4）现有的测试方法由于缺少应用特定的领域知识，无法生成有效的用户输入，导致测试覆盖率不高.基于以上原因，大量的应用在没有经过充分测试后发布，兼容性问题频发.针对以上问题，提出一种基于录制/重放的Android应用众包测试方法，并实现了原型工具AppCheck.AppCheck收集众包用户和设备交互时所产生的事件序列后，将其转换为平台无关的测试脚本，可直接在众包用户的设备上进行重放.在重放期间，AppCheck收集各种测试相关数据（例如截图和布局信息）以检测兼容性问题.实验结果表明，AppCheck能够有效地完成跨设备录制/重放以及兼容性问题的检测，弥补了当前方法的不足.

摘要:使用对称正定（symmetric positive definite，简称SPD）矩阵将视觉数据建模到黎曼流形（SPD流形），对于模式识别和机器学习中许多任务有较好的效果.其中，将基于稀疏表示的分类算法扩展到SPD流形上样本的分类任务得到了广泛的关注.本文综合考虑了稀疏表示分类算法的特点以及SPD流形的黎曼几何结构，通过核函数将SPD流形嵌入到再生核希尔伯特空间（reproducing kernel Hilbert space，简称RKHS），分别提出了核空间潜在稀疏表示模型和潜在分类方法.但是，原始的视觉数据在核空间中没有明确的表示形式，这给核空间中的潜在字典更新带来了不便.Nyström是一种可以近似表征核特征的方法.因此，我们利用该方法得到训练样本在RKHS中的近似表示，以更新潜在字典和潜在矩阵.最后，通过在5个标准数据集上的分类实验，验证了该方法的有效性.

摘要:游客倾向于采用个性化的旅游路线，规划这样的路线需要综合考量路径长度、路径开销和路径覆盖的兴趣点.关键词覆盖最优路径查询（KOR）就是用于规划这样的路线的一类查询，其处理过程通常包括预处理和路径拓展.由于路网图规模的不断扩大，现有算法预处理所需内存开销急剧上升，由于内存不足，导致较大规模的路网不能处理；路径拓展搜索空间快速膨胀，应用场景可扩展性与查询实时性难以保证.针对这些问题，提出一种大规模路网图下关键词覆盖最优路径查询算法KORL.KORL在预处理阶段将路网划分为若干子图，仅保存子图内路径和子图之间路径的信息，以减小预处理所需内存.在路径拓展阶段，综合运用最小代价剪枝、近似支配剪枝、全局优先拓展和关键词顶点拓展等策略对现有算法进行优化，以高效地搜索近似最优解.采用美国各地区的路网图，在16G内存环境下进行实验，突破了现有算法只能处理顶点数不超过25K路网图的限制.实验结果表明，KORL算法具有良好的可扩展性.

摘要:为了解决联盟区块链平台中的隐私保护问题，提出了一种基于双层协同的隐私数据保护方法，包括：（1）链间隐私保护：通过将不同业务的数据进行分流处理、分区存储，实现了不同业务之间的隐私机密性保护；（2）链内隐私保护：通过在交易体中嵌入字段来指定链内隐私数据的参与方，并由接收交易的区块链节点作为中转节点进行链内隐私数据的同步，中转节点同时负责将隐私数据替换成其哈希值后，构造公开交易进行正常公开交易的上链，待公开交易上链成功后，由隐私参与方节点各自进行隐私账本的更新.为了验证该方法的有效性，分别对链间隐私方法吞吐量以及链内隐私保护方法的延迟性进行了测试与对比，结果表明，通过结合粗粒度的链间隐私保护与细粒度的链内隐私保护，在满足了隐私需求的同时，也保证了可观的性能，为区块链平台的隐私性与安全性做出了贡献.

摘要:随着互联网规模的不断增大，网络管理和运维变得极其复杂，网络自治成为未来网络发展的趋势，基于意图的网络（intent-based networking，简称IBN）应运而生.首先从IBN的定义入手，介绍学术界及产业界对IBN范畴及体系结构的描述，并概述IBN实现的闭环，包括意图获取、意图转译、策略验证、意图下发与执行、实时反馈及优化；其次，按照IBN闭环，详细阐述IBN关键技术的研究现状；随后，举例说明IBN在网络测量和网络业务编排中的应用；最后，展望未来研究工作并总结全文.

摘要:医学图像分割是计算机辅助诊断的关键技术.青光眼作为全球第二大致盲眼病，其早期筛查和临床诊断依赖于眼底图的视盘和视杯的准确分割.但传统的视盘和视杯分割方法采用人工构建特征，模型泛化能力差.近年来，基于卷积神经网络的端对端学习模型可通过自动发现特征来分割视盘和视杯，但由于标注样本有限，模型难以训练.提出一个基于半监督条件生成对抗网络的视盘和视杯两阶段分割模型——CDR-GANs.该模型的每个分割阶段均由语义分割网络、生成器和判别器构成，通过对抗学习，判别器引导语义分割网络和生成器学习眼底图及其分割图的联合概率分布.在真实数据集ORIGA上的实验结果表明，CDR-GANs在均交并比（mean intersection over union，简称MIoU）、CDR绝对误差（absolute CDR error）和实际分割效果这些指标上明显优于现有模型.

摘要:随着异构计算技术的不断进步，CPU和GPU等设备相集成的异构融合处理器在近些年得到了充分的发展，并引起了学术界和工业界的关注.将多种设备进行集成带来了许多好处，例如，多种设备可以访问同样的内存，可以进行细粒度的交互.然而，这也带来了系统编程和优化方面的巨大挑战.充分发挥异构融合处理器的性能，需要充分利用集成体系结构中共享内存等特性；同时，还需结合具体应用特征对异构融合处理器上的不同设备进行优化.首先对目前涉及异构融合处理器的研究工作进行了分析，之后介绍了异构融合处理器的性能分析工作，并进一步介绍了相关优化技术，随后对异构融合处理器的应用进行了总结.最后，对异构融合处理器未来的研究方向进行展望，并进行了总结.