程序条件化用于软件模型检测中的状态空间缩减

针对软件模型检测中的状态爆炸问题，提出将程序条件化技术用于软件状态空间缩减的方案．以程序性质的线性时序逻辑公式可能出现的蕴涵式的前件作为条件化的约束条件，通过分析程序符号化执行语义，借助自动定理证明器，对语句的可达性条件进行逻辑推理，删除那些与性质的可满足性无关的语句，以达到程序精简的目的．理论分析和实验结果表明，条件化可以有效缩减程序状态空间，而且缩减后的程序模型保留了原程序中与所需验证的性质有关的所有信息，满足软件模型检测对状态缩减的安全性要求．     

基于Windows API调用序列的恶意代码检测方法

为解决现有恶意代码检测方法存在的特征提取能力不足、检测模型泛化性弱的问题，提出了一种基于Windows API调用序列的恶意代码检测方法.使用N-gram算法和TF-IDF算法提取序列的统计特征，采用Word2Vec模型提取语义特征，将统计特征和语义特征进行特征融合，作为API调用序列的特征.设计了基于Stacking的三层检测模型，通过多个弱学习器构成一个强学习器提高检测模型性能.实验结果表明，提出的特征提取方法可以获得更关键的特征，设计的检测模型的准确率、精确率、召回率均优于单一模型且具有良好的泛化性，证明了检测方法的有效性.     

基于自相似特性的恶意代码动态分析技术

在比较恶意代码的分析技术的基础上,将自相似特性技术引入恶意代码的动态分析中。跟踪同类型的恶意程序,采集API函数的调用序列,提取关键特征信息,得到时间调用序列,并进行归一化处理。通过重新标度权差分析算法、回归方差算法和Higuchi算法,分别计算程序的Hurst指数,匹配同种恶意程序的自相似性。将恶意程序与正常程序的API调用序列和Hurst指数进行对比实验表明,恶意程序调用API函数与正常程序存在差异,并且同一类型的恶意程序确实具有自相似性,从而能够动态检测出恶意程序。     

基于概念分析的软件横切关注点提取方法

为解决软件遗产系统中横切特性的理解和进化问题，提出了面向侧面的逆向工程框架模型，并以此为基础给出了一种用例驱动的形式化概念分析方法，对需求分析模型层面上的系统横切特性进行逆向恢复．通过对目标系统执行信息进行概念格分析，文中方法能够识别和提取横切用例模型的系统方法调用集合，并将它们抽象为系统的早期侧面．和仅为了代码重构而进行的侧面挖掘技术相比，该方法更适合在较高的系统抽象层面上进行程序理解．作为一种采用增量式结果产生策略的半自动化方法，它的实施流程也具有更好的可控性和对逆向工程需求变化的适应性．     

基于语义分析的网络爬虫模型的研究

针对传统通用网络信息采集系统自身固有的缺陷,根据语义分析的相关理论,本文提出了基于语义的网络爬虫的相关模型,该模型构建知识概念集合,并对其进行关键字切割与划分,生成能表达主题的主题关键词集合。结合中国《知网》的相关理论与技术,对传统抓取的网页在语义的角度进行分析,对已抓取的网页页面内容及其中链接的扩展元数据等相关信息进行分词及语法语义等相关处理,获取网页内容关键词集合及超链接的关键词集合,然后分别对获取的网页内容关键词与链接关键词进行与主体关键词集合采用语义分析算法进行语义相关性的判定,保存需要的网页,并预测及提取与主题相关的URL,从而提高网络资源信息采集相关率。     

基于自适应攻击树的木马检测方法

本文研究并总结出木马攻击行为的规律,通过静态分析PE文件提取出程序运行时调用的API,用木马攻击中常见的危险系统调用序列来建模一个动态攻击树,将分析PE文件得到的API调用集合与建立的攻击树进行匹配,有效的区分木马文件和正常文件,并能根据检测结果对攻击树进行动态的调整,以不断提高攻击树对未知病毒的检测能力。     

基于自适应攻击树的木马检测方法

本文研究并总结出木马攻击行为的规律,通过静态分析PE文件提取出程序运行时调用的API,用木马攻击中常见的危险系统调用序列来建模一个动态攻击树,将分析PE文件得到的API调用集合与建立的攻击树进行匹配,有效的区分木马文件和正常文件,并能根据检测结果对攻击树进行动态的调整,以不断提高攻击树对未知病毒的检测能力。     

Prolog的语义保持变换

程序变换方法在逻辑程序中的应用主要是基于这样的理论结果,即Fold/Unfold变换保持了逻辑程序的最小Herbrand模型语义和答复转换集语义,但是当逻辑程序的实现采用标准Prolog系统的最左计算规则和深度优先查找规则时,变换后的程序未必能保持原程序的语义,此外,程序的语义等价性证明也往往是难以理解和阅读的,为此,首先用与计算SLD－树叶结点有关的答复置换序列算法的方式,引入一个相对易于理解的Prolog语义定义,然后给出有关的语义保持变换规则并加以证明。     

垃圾邮件过滤中潜在语义索引的应用

将潜在语义索引(LSI)应用于垃圾邮件过滤领域,并将其与向量空间模型(VSM)和经典的邮件过滤器Spa-mAssassin系统进行比较.另外,对基于词提取技术的邮件文本特征集合和SpamAssassin系统提取的邮件"元特征"集合进行了对比.实验结果表明,LSI与VSM均取得了较SpamAssassin系统更优的分类效果.     

基于离线汇编指令流分析的恶意程序算法识别技术

识别二进制程序中的算法,在恶意程序检测、软件分析、网络传输分析、计算机系统安全保护等领域有着广泛的应用和重要的意义。该文提出基于离线汇编指令流分析的恶意代码算法识别技术,综合运用二进制插桩、污点跟踪、循环识别等技术,从行为语义、关键常数2个维度对程序进行描述,并且分析提取特征。算法识别模型使用机器学习算法,针对双维度特征生成初阶识别模型,并通过模型融合优化识别效果,实现对广义程序算法的高准确率识别。     

基于改进Transformer的生成式文本摘要模型

基于循环神经网络(recurrent neural network,RNN)注意力机制的序列到序列模型在摘要信息提取服务中已经取得了较好的应用,但RNN不能较好地捕捉长时序信息,这使现有模型受限。为此,提出了基于改进Transformer的生成式文本摘要模型。该模型利用Transformer提取全局语义,使用局部卷积提取器提取原文细粒度特征,并设计全局门控单元以防止信息冗余和弥补语义不足,筛选出利于摘要生成的文本关键信息。实验结果表明,所提模型在大规模中文短文本摘要数据集(large scale Chinese short text summarization,LCSTS)上的效果有明显的提升,在电力运维摘要数据集上,也有良好效果,具有可扩展性。     

线性混合系统的一种验证方法

混合系统是指嵌入于物理环境中的数字实时系统．由于计算机技术的快速发展,混合系统在各行各业中都得到广泛应用,但是由于混合系统涉及到连续时间,因此其验证问题始终没有得到完善的解决．近年来,人们普遍采用模型检验方法对混合系统进行验证．由于线性混合系统在实际应用中可以表示大多数的嵌入式实时系统,因此我们着重研究这类混合系统的验证算法．本文首先介绍了混合系统的模型—混合自动机,然后提出了一种针对线性混合系统的基于区域的先划分再遍历的半确定性验证方法．经实例检验,该方法能够有效地验证线性混合系统．最后将本文的方法同有关的其它算法进行了比较     

基于超图文法的软件体系结构动态演化

提出用带约束的超图表示软件体系结构,给出基于超图态射的软件体系结构动态演化通用产生式规则的形式化语义和操作,定义类型超图作为体系结构风格,运用超图文法和体系结构风格建模软件体系结构动态演化.为了验证软件体系结构动态演化的正确性,采用模型检测技术,设计算法对软件体系结构动态演化性质进行形式化验证,并应用模型检测工具进行实验分析.该方法既提供了图形化的直观表示,又展示了基于文法的形式化理论框架.     

空问映射与响应面法相结合的改进优化算法

在空间映射与响应面法相结合的基础上修改了序列响应面的程序流程，从而改变了应用响应面方法优化时的迭代本质。改进方法无须每次迭代重新拟合低保真模型响应面，只在第一次迭代拟合响应面，在此基础上调整高低保真模型设计变量间的映射关系，优化收敛更迅速。由于避免了反复的试验设计和模型分析，改进方法的计算效率远高于原方法。数值算例表明了该方法的稳定性，此方法可以大大减少应用序列响应面进行优化或可靠性评价的计算量。     

基于CTL的并发系统CSP模型验证

主要通过指称语义和回答集程序(Answer Set Programming,简称ASP)完成迹模型的生成,并构建了一套基于计算树逻辑(computing tree logic,简称CTL)的CSP模型验证方法.实验表明,该方法对于分支类型的性质具有较好的描述能力,且保证了验证的正确性.     

基于GRNN的RGB到L＊a＊b＊色彩空间的转换模型

针对目前色彩空间转换精度低的问题,建立了一种基于广义回归神经网络（GRNN）的色彩空间转换模型．将RGB色彩空间进行分割,并将RGB值用Adobe Photoshop软件中的拾色器进行手工转换,得到对应的L＊a＊b＊值,从而得到建模样本和检验样本数据．用MATLAB7．5软件编程,建立RGB到L＊a＊b＊色彩空间的转换模型,并对其转换精度进行评价．检验结果表明,该转换模型精度高且训练速度极快,可应用于色彩管理的相关技术领域．     

Abstract model checking for Web services

Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.     

Rigorous Modeling of Real-time System Based on UML and PVS

Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an industrial standard modeling language which provides a powerful expressi-veness, intuitive and easy to use interface to model. UML is widely accepted by software developer. However, for lack of precisely defined semantics, especially on the dynamic diagrams, UML model is hard to be verified. PVS is a general formal method which provides a high-order logic specification language and integrated with model checking and theorem proving tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time system. In this approach, we provide 1) a timed extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexible and friendly in modeling, extendable in formalization and verification content, and better performance. Time constraints are modeled and verified and its a highlight of this paper.