摘要:

摘要:程序终止性问题是自动程序验证领域中的一个研究热点.秩函数探测是进行终止性分析的主要方法.针对单重无条件分支的多项式循环程序，将其秩函数计算问题归结为二分类问题，从而可利用支持向量机（SVM）算法来计算程序的秩函数.与基于量词消去技术的秩函数计算方法不同，该方法能在可接受的时间范围内探测到更为复杂的秩函数.

摘要:根据权威统计数据，软件测试中发现的70%以上的错误由需求获取或体系结构设计引起.因此，应用软件体系结构在设计阶段的正确性验证非常重要.现有的软件体系结构设计方法不支持需求满足验证，需求满足验证需要其他验证工具的支持.面向主流Web应用软件的体系结构设计及其需求满足验证，提出了一种高阶类型化软件体系结构建模和验证语言（SAML）与软件体系结构建模和验证方法（SAMM）.SAML语言通过定义类型和项的语法及语义，描述软件体系结构中类型和对象的构造，通过定义类型规则及其类型检查算法来判定Γ|-t：T和Γ|-R（T₁，T₂）是否成立.SAMM给出了软件体系结构建模范式，包括构建接口类型M_cls（type interface）、组件M_cmpt（component）、容器M_cont（container）、框M_frm（frame）和框架M_frwk（framework）这5层建模过程，以及生成层内与层间类型之间关系对应的类型规则，同时定义了接口类型方法调用图（G_SA）用以刻画软件体系结构设计要求，定义了类型序列及其正确性用以刻画需求期望的性质，并给出了相应的验证算法.设计实现了基于该方法的原型工具系统SAMVS，其中，模型编辑环境支持应用软件的设计过程，验证环境支持设计满足需求的自动化验证.通过一个实际案例，完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.

摘要:近年来，基于Petri网可覆盖性的验证技术已经成功地应用于并发程序的验证与分析中.然而，由于Petri网的可覆盖性问题复杂度太高，这类技术在应用时有较大的局限性，对于输入规模较大的问题常常会出现超时的情况.而Petri网的一个子系统——非交互式Petri网，其可覆盖性和可达性复杂性均是NP完备的，同时表达力又可以作为某类并发程序的验证模型.设计并实现了可以高效验证非交互式Petri网可覆盖性的工具CFPCV.采用基于约束的方法，从模型中提取约束，并使用Z3 SMT求解器对约束进行求解，同时，通过子网可标记方法对候选解进行验证，从而保证每组解都是正确解.通过实验分析了该工具的成功率、迭代次数以及运行效率，发现该算法不仅验证成功率高，而且性能非常优异.

摘要:时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑.扩展线性时段不变式是时段演算的重要子集.针对实时自动机，提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法.该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题，从而可以采用量词消去技术进行求解.首先，运用符号化的思想，在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段；然后，将每条符号化路径片段转化为一个量词线性算术公式；最后，利用量词消去工具求解.与已有工作相比，基于实时自动机设计了验证算法.另外，降低了验证复杂度，并且加速了验证过程的实际速度.

摘要:信息物理系统（cyber-physical system，简称CPS）是一个在环境感知的基础上整合了物理和计算元素的系统，它可以智能地响应真实世界的动态变化，具有重要而广阔的应用前景.然而，CPS工作在复杂的物理环境中，周围的物理变化会对CPS的行为产生影响.因此，确保CPS在复杂环境中的安全性和可靠性至关重要.提出了一种面向实时数据的一体化建模方法，通过定义一系列的规则，将领域环境模型组合到运行时验证过程中去，从而保证CPS在不确定环境中的安全性和可靠性.该方法首先为环境建立数学模型.然后，设计合并规则将相同系统参数下仅有一个环境影响因子的数学模型合并为相同系统参数下有一个或多个环境影响因子的数学模型.之后，定义转换规则，将数学模型转换为伪代码表示的环境模型.最后，根据组合规则将环境模型组合到运行时监视模型中执行验证.该方法使得监视模型更加完整、准确，当环境发生变化时，通过动态调整参数范围使得CPS中的安全属性在复杂的物理环境中仍然得以满足.将该方法应用到移动机器人避障实验中，对影响电池容量的温度和湿度进行数学建模，然后将环境模型组合到监视模型中去，最终实现在执行任务前可以根据不同的物理环境准确地给出续航时间安全提醒.

摘要:随着安全关键系统对计算性能要求的日趋提高，能够提供更强计算能力而又减少电子设备的体积、重量和功耗的多核处理器将在安全关键领域得到广泛应用.同步语言能够表达确定性并发行为且具有精确时间语义等特性，适用于安全关键软件的建模和验证.目前，同步语言SIGNAL编译器主要支持串行代码生成，较少关注多线程代码生成.提出一种同步语言SIGNAL多线程代码生成工具.首先将SIGNAL程序转换为经过时钟演算的S-CGA中间程序；之后将S-CGA中间程序转换为时钟数据依赖图以分析依赖关系；然后对时钟数据依赖图进行拓扑排序划分，并针对划分结果提出优化算法和基于流水线方式的任务划分方法；最后将划分结果转换为虚拟多线程结构并进一步生成可执行多线程C/Java代码.通过在多核处理器上的实验，验证了所提方法的有效性.

摘要:同步数据流语言（如Lustre、Signal）在航空、高铁、核电等安全关键领域得到广泛应用.例如，适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言.这类语言相关开发工具，特别是编译器的安全性问题也自然受到高度关注.近年来，基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一，也取得了瞩目的成果，如CompCert项目实现了产品级的可信C编译器.同样，人们也采用这种方法开展了同步数据流语言可信编译器的研发工作.主要关注从事这一工作的两个长线项目，二者均研发面向基于Lustre的同步数据流语言编译器，分别以Vélus和L2C代称.对Vélus和L2C从多个重要的角度进行较为深入的分析与比较.

摘要:信息物理系统（cyber-physical systems，简称CPS）是基于环境感知实现计算、通信与物理元素紧密结合的下一代智能系统，广泛应用于安全攸关的系统和工业控制等领域.信息技术与物理世界的相互作用使得CPS容易受到各种恶意攻击，从而破坏其安全性.主要研究存在瞬态故障的CPS中传感器的攻击检测问题.考虑具有多个传感器测量相同物理变量的系统，其中一些传感器可能受到恶意攻击并提供错误的测量.此外，使用抽象传感器模型，每个传感器为控制器提供一个真实值的可能间隔.已有的用于检测传感器被恶意攻击的方法是保守的.当专业攻击者在一段时间内轻微地或不频繁地操纵传感器的输出时，现有方法很难捕获到攻击，如隐身攻击.为了解决这个问题，设计了一种基于融合间隔和历史测量的传感器攻击检测方法.该方法首先为不同的传感器构建不同的故障模型，使用系统动力学方程把历史测量融入到攻击检测方法中，从不同的方面分析传感器的测量.另外，利用历史测量和融合间隔解决了两个传感器的测量相交时是否存在故障的问题.该方法的核心思想是利用传感器之间的成对不一致关系检测和识别攻击.从EV3地面车辆上获得真实的测量数据来验证算法的性能.实验结果表明，所提出的方法优于现有方法，对各种攻击类型都有较好的检测和识别性能，特别是对于隐身攻击，检测率和识别率大约提高了90%以上.

摘要:自动机的重置序列也称为同步序列，具有以下特性：有限自动机通过运行重置序列w，可从任意一个未知的或无法观测到的状态q₀到达某个特定状态q_w.这仅依赖于w，而与开始运行w时的状态q₀无关.这一特性可用于部分可观察的复杂系统的自动恢复，而无需重启，甚至有时不能重启.基于此，重置问题自出现以来便得到关注和持续研究.最近几年，它被扩展到可以描述诸如分布式、嵌入式实时系统等复杂系统的无限状态模型上，比如时间自动机和寄存器自动机等.以时间自动机的重置问题的计算复杂性为研究对象，发现重置问题与可达性问题有着紧密的联系.主要贡献是：（1）利用时间自动机可达性问题的最新成果，完善完全的确定的时间自动机重置问题的计算复杂性结论；（2）对部分规约的确定的时间自动机，研究得出，即使在输入字母表大小减至2的情况下，其复杂性仍是PSPACE-完全的；特别地，在单时钟情况下是NLOGSPACE-完全的；（3）对完全的非确定的时间自动机，研究得出其D_i-可重置问题（i=1，2，3）是不可判定的，其重置问题与非确定的寄存器自动机重置问题在指数时间可以相互归约，通过证明指数时间归约相对高复杂性类具有封闭性，利用非确定的寄存器自动机的结论得出单时钟的时间自动机的重置问题是Ackermann-完全的、限界的重置问题是NEXPTIME-完全的.这些复杂性结论，说明关于时间自动机的重置问题大都是难解的，一方面，为时间系统的可重置性的检测和求解奠定坚实的理论基础，另一方面，为以后寻找具有高效算法的特殊结构的时间系统（即具有高效算法的问题子类）给予理论指导.

摘要:人们理解自然语言通常是在篇章级进行的，随着词汇级及句子级研究的日益成熟，自然语言处理研究的焦点已转向篇章级.篇章分析的主要任务就是从整体上分析出篇章结构及其构成单元之间的语义关系，并利用上下文理解篇章.根据不同的篇章分析目的，篇章单元及其关系可以表示为不同的篇章基本结构，不同篇章基本结构及其关系的研究可提供不同层面的篇章理解.目前对汉语篇章内在规律的研究较少，缺乏对篇章进行有效分析和深入理解的理论方法体系，这严重制约了篇章级的相关研究及应用.重点关注篇章的两个最基本特征，即衔接性和连贯性，从篇章结构分析的理论研究、资源建设和计算模型这3个方面，分别探讨篇章修辞结构（体现篇章连贯性）和话题结构（体现篇章衔接性），对篇章理解的国内外研究现状进行了归纳和整理，并给出了目前存在的主要问题和研究趋势.

摘要:概率图模型是目前机器学习研究的热点，基于概率图模型构造的生成模型已广泛应用于图像和语音处理等领域.受限玻尔兹曼机（restricted Boltzmann machines，简称RBMs）是一种概率无向图，在建模数据分布方面有重要的研究价值，RBMs既可以结合卷积算子构造深度判别模型，为深度网络提供统计力学的理论支持，也可以结合有向图构建生成模型，提供具有多峰分布的先验信息.主要综述了以RBMs为基础的概率图模型的相关研究.首先介绍了基于RBMs的机器学习模型的基本概念和训练算法，并讨论了基于极大似然估计的各训练算法的联系，比较了各算法的log似然损失；其次，综述了RBMs模型最新的研究进展，包括在目标函数中引入对抗损失和W距离，并构造基于RBMs先验的变分自编码模型（variational autoencoders，简称VAEs）、基于对抗损失的RBMs模型，并讨论了各实值RBMs模型之间的联系和区别；最后，综述了以RBMs为基础的模型在深度学习中的应用，并讨论了神经网络和RBMs模型在研究中存在的问题及未来的研究方向.

摘要:情绪分析是细粒度的情感分析任务，其目的是通过训练机器学习模型来判别文本中蕴含了何种情绪，是当前自然语言处理领域中的研究热点.情绪分析可细分为情绪分类与情绪回归两个任务.针对情绪回归任务，提出一种基于对抗式神经网络的多维度情绪回归方法.所提出的对抗式神经网络由3部分组成：特征抽取器、回归器、判别器.该方法旨在训练多个特征抽取器和回归器，以对输入文本的不同情绪维度进行打分.特征抽取器接受文本为输入，从文本中抽取针对不同情绪维度的特征；回归器接受由特征抽取器输出的特征为输入，对文本的不同情绪维度打分；判别器接受由特征抽取器输出的特征为输入，以判别输入的特征是针对何情绪维度.该方法借助判别器对不同的特征抽取器进行对抗式训练，从而获得能够抽取出泛化性更强的针对不同情绪维度的特征抽取器.在EMOBANK多维度情绪回归语料上的实验结果表明，该方法在EMOBANK新闻领域和小说领域的情绪回归上均取得了较为显著的性能提升，并在r值上超过了所有的基准系统，其中包括文本回归领域的先进系统.

摘要:随着开源软件的兴起及软件开发支撑工具的普及，Internet上积累了大量开放的软件开发活动数据，越来越多的实践者与研究者尝试从中获取提高软件开发效率和产品质量的洞察.为了提高数据分析的效率、方便分析结果的重现与对比，许多工作提出了构建与使用共享数据集.然而，现有软件开发活动数据集的构建过程可追溯性差、适用范围窄，对数据随时间、环境发生的变化欠考虑.这些不足直接威胁数据的质量及分析结果的有效性.针对该问题，提出一种层次化、多版本化的方法来构建与使用软件开发活动数据集.层次化是指在数据集中包括收集和后续处理所得的原始、中间和最终数据，建立数据集的可追溯性并扩展其适用范围.多版本化是指通过多种方式进行多次数据收集，使数据使用者能够观察到数据的变化，为数据质量及分析结果有效性的验证和提高创造条件.通过基于该方法构建的Mozilla问题追踪数据集进行示范，并验证了该方法能够帮助数据使用者高效地使用数据.

摘要:随着互联网的迅猛发展，网络广告成为互联网最重要的商业模式之一.网络广告在促进互联网发展的同时，也带来了用户信息泄露、影响用户网页浏览体验等负面问题.为了对网络广告进行系统的研究，需要获取广告生成过程中完整的调用路径.由于加载到页面中的JavaScript文件量大、函数调用路径链路长、路径中的JavaScript代码经过了一定的压缩和混淆，因此很难通过静态方法获取网络广告调用路径.分析了动态广告生成的过程，对相关代码进行动态插桩，利用函数参数实现广告调用信息的传递，并记录下每个iframe内部的调用信息，通过匹配与合并多个iframe的信息，生成了完整的广告调用路径并确定了广告插入的操作方式.针对21个真实网站进行了实验，结果表明：该方法能够在不太影响性能的前提下，获取到静态方法无法获取到的广告动态加载过程信息并生成广告代码调用路径.

摘要:知识图谱是人工智能的重要基石.各领域大规模知识图谱的构建和发布对知识图谱数据管理提出了新的挑战.以数据模型的结构和操作要素为主线，对目前的知识图谱数据管理理论、方法、技术与系统进行研究综述.首先，介绍知识图谱数据模型，包括RDF图模型和属性图模型，介绍5种知识图谱查询语言，包括SPARQL、Cypher、Gremlin、PGQL和G-CORE；然后，介绍知识图谱存储管理方案，包括基于关系的知识图谱存储管理和原生知识图谱存储管理；其次，探讨知识图谱上的图模式匹配、导航式和分析型3种查询操作.同时，介绍主流的知识图谱数据库管理系统，包括RDF三元组库和原生图数据库，描述目前面向知识图谱的分布式系统与框架，给出知识图谱评测基准.最后，展望知识图谱数据管理的未来研究方向.

摘要:随着Internet的普及，各类社交网络走进人们的视野，用户为满足不同的服务需求，往往不会局限于单一社交网络中，因此，跨社交网络环境下的用户识别问题成为研究者的热门话题.主要利用网络结构信息，针对社交网络对齐问题进行研究，主要包含以下研究点：首先，将网络对齐问题抽象为最大公共子图问题（α-MCS），并提出求解自适应参数α的方法，相比于传统的基于启发式定义参数α的方法，该方法可有效区分不同类型网络中匹配用户与非匹配用户；其次，为快速而准确地解决α-MCS，提出了基于最大公共子图的迭代式网络对齐算法MCS_INA（α-MCS based iterative network alignment algorithm），该算法每次迭代过程主要包含两个阶段.第1个阶段，分别在两个社交网络中选取各自的候选匹配用户，第2个阶段，针对候选匹配用户进行识别.相比于其他算法，MCS_INA时间代价低，且依据不同网络特征，通过参数估计，可保证较高的识别精度；最后，在真实数据集和合成数据集中验证了算法MCS_INA的有效性.

摘要:近年来，人脸属性估计因其广泛的应用而得到了大量的关注和研究，并且很多估计方法被提了出来.主要对现有相关工作进行归纳总结，为研究者提供相关参考.首先，根据是否考虑人脸性别、年龄、人种等不同属性间的内在关联，将现有的人脸面部属性研究方法划分成朴素的研究方法和自然的研究方法这两大类进行总结介绍.然后，从单一人脸数据库标记不完备、现有方法未能完备利用多属性联合估计、现有方法未能很好地利用各面部属性间关系这3个方面阐述当前方法的不足.最后，给出关于人脸面部属性估计进一步的研究方向.

摘要:弹性运动估计是近年来出现的一种有效的时间维视频预测编码技术，但其基于高斯-牛顿法的优化求解仍存在计算量高、收敛不稳定的问题.为此提出一种基于改进Levenberg-Marquardt（L-M）法的弹性运动估计算法.首先，根据弹性基函数和黑塞矩阵的数值对称性，给出了L-M黑塞矩阵的快速计算方法，将其计算量降低了62.5%.其次，通过理论和实验分析发现，L-M对角矩阵阻尼系数的更新因子对弹性运动估计性能有明显影响，进而采用最近2次迭代的搜索步长的平方商自适应地确定更新因子，并对该阻尼系数进行正、负交替更新.实验结果表明，对于具有不同空间分辨率和场景特点的视频序列，算法始终能够保持较高的估计精度，运动补偿的平均峰值信噪比较之基于块平移模型的全搜索和基于改进高斯-牛顿法的弹性运动估计分别提高2.54dB、1.77dB.并且，所提算法收敛速度快，一般只需1~2次迭代就能取得高于传统弹性运动估计和块平移全搜索的峰值信噪比.