有界模型检测的优化

G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-time temporal logic,简称LTL)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成SAT(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值.

一种知识图谱的排序学习个性化推荐算法

推荐系统是解决"信息过载"的有效方法,提出一种知识图谱的排序学习个性化推荐算法.本文算法首先构建融合上下文信息的知识图谱,使用基于深度学习的网络表示方法 Node2Vec抽取知识图谱特征,通过将排序学习模型产生的反馈模型与用户兴趣迁移模型结合,构建混合推荐模型,最终通过排序学习进行Top-N推荐.该算法能够将各种不同性质的上下文特征结合在一起,并通过排序学习衡量这些多维特征的权重比例,解决了不同特征的融合问题,并且能够考虑到用户兴趣迁移和长短期偏好.在Movielens 1M数据集上的对比实验验证文中算法的有效性,实验表明,该算法能够有效提高推荐的P@N和MAP值.

基于概率模型的Raft协议形式化验证

共识协议作为分布式系统的关键要素和核心组件,用于解决分布式场景下可能出现故障的节点间保证同一数据一致的问题,其准确性和高效性直接决定了系统的性能。Raft共识协议是目前分布式系统中常见且有效的算法。本文首先使用概率模型检测方法对Raft共识协议进行形式化建模,然后利用概率模型检测的属性规约技术对它的相关属性进行描述,最后通过模型检测工具验证并分析Raft共识协议的一致性和高效性。实验结果表明,Raft共识协议满足一致性,但是在领导者选举阶段,当跟随者维护的最新日志序号的差值范围增加时,选举回合数也会增多,使得整个服务周期选举时间增加,从而影响协议的执行效率。

SAT问题中局部搜索法的改进

局部搜索方法在求解SAT问题的高效率使其成为一研究热点.提出用初始概率的方法对局部搜索算法中变量的初始随机指派进行适当的约束.使在局部搜索的开始阶段,可满足的子句数大大增加,减少了翻转的次数,加快了求解的速度.用该方法对目前的一些重要的SAT问题的局部搜索算法(如WSAT,TSAT,NSAT,SDF等)进行改进,通过对不同规模的随机3-SAT问题的实例和一些不同规模的结构性SAT问题的实例,以及利用相变现象构造的难解SAT实例测试表明,改进后的这些局部搜索算法的求解效率有了很大的提高.该方法对其他局部搜索法的改进具有参考价值。

基于Adaboost与Clifford代数的人脸检测

Adaboost算法在光照不均、背景复杂的条件下进行人脸检测时误检率较高。为解决该问题,提出一种基于Adaboost算法与Clifford代数矢量积性质的人脸检测方法。利用Adaboost算法初步定位人脸可能存在的区域,对该区域进行基于知识的校验,如果校验失败,根据Clifford矢量积性质,寻找与待验证区域相似度较高的人脸,当相似度大于阈值时,判断其为人脸。实验结果表明,与Viola-Jones方法相比,该方法在保持较高检测率的同时,降低了误检率,且鲁棒性较好。

网络课程中基于Web的在线测试系统的研究与实现

设计了一个基于Web的在线测试系统,并成功应用于网络课程的教学活动中。同时,设计了一个高效率自动组卷算法。介绍了该系统的功能、结构、关键技术和自动组卷算法。该系统在其他的相关领域也有较重要的参考价值。

离散正交S变换在人脸识别中的应用研究

人脸识别是模式识别领域的一个重要研究方向,有着广泛的应用前景.由于人脸图像受到光照、表情等因素的影响,在空间域直接使用线性方法具有一定的局限性,因此,从人脸特征的角度出发,提出一种新的人脸识别方法,即基于离散正交S变换(Discrete Orthonormal S-Transform,DOST)特征的人脸识别算法.首先,对人脸图像进行二维离散正交S变换得到人脸图像的特征,然后通过主成分分析对特征矩阵进行降维,提取特征向量,形成特征矩阵,最后用支持向量机分类识别.通过相应的实验证明本文提出的算法提高了识别的精确度和识别的速度.

PDA上实现遥控器的集成

在PDA上通过二次开发，利用PDA的红外线端口，接收和发射遥控器产生的红外线，使PDA可替代遥控器。文章介绍了该系统的开发和应用环境以及系统实现的原理。

网络课程中短消息平台的开发及应用

论文设计一个基于ActiveX控件的短消息平台,并把它应用于网络课程中,很好促进了教学活动。论文主要介绍这个短信平台的基本原理、实现方法和一些关键的技术问题。同时,这种短信平台对许多相关领域有较高实用价值。

公平交换协议的信道可信度形式化验证方法

公平交换协议是一种重要的电子商务安全协议,已有的针对公平交换协议进行的形式化验证只能定性分析协议是否满足给定性质,本文提出基于信道可信度的公平交换协议的形式化验证方法,重点对信道问题进行定量分析.以一个电子合同签署协议为例,通过概率模型检测的方法对协议建立离散时间马尔可夫链模型,用概率计算树逻辑对协议属性进行描述,通过PRISM概率模型检测工具对协议进行定量的验证和分析.实验结果表明公平交换协议各实体间信道可信度对协议的公平性、有效性和时限性有不同程度的影响,对相应信道进行控制或改善可以提高协议安全性.

基于GSM短消息的监控系统的研究与实现

设计并实现一个基于GSM短信息的监控报警系统,介绍了该系统的原理和结构,并详细阐明了其实现方法及一些关键的技术.实践证明,系统具有运行可靠、费用低廉等特点,有较高的应用价值.

基于Curvelet变换特征的人脸识别算法

针对小波变换无法准确表达二维奇异曲线的弱点,提出基于曲波(Curvelet)变换特征的人脸识别算法。Curvelet变换可以很好地去逼近奇异曲线,对于人脸图像能实现最优的稀疏表示。该算法采用基于Wrapping的离散Curvelet变换加权算法对训练集的人脸图像进行特征提取生成特征矩阵,再通过PCA方法降低维数后结合稀疏表示分类算法(SRC)进行人脸识别。通过在ORL、Yale和AR三个人脸数据库上的仿真实验以及和基于小波变换类识别算法、LDA算法和SRC算法等比较,实验结果表明该算法在人脸遮挡、姿态变换、表情变换和光照变换等干扰因素的作用下具有较高的人脸识别率和较好的鲁棒性。

一种基于多模式加密算法的文件保护方案

结合对称密码算法中的DES、IDEA、AES和单向散列算法中的MD5、SHA-1、SHA-256等算法,提出了一种在同一文件内部采用多模式加密的方案,该方案比传统的单一模式加密的方案能更好地保证数据的完整性和安全性。详细描述了该方案的算法实现,通过试验验证了其实用性,同时分析了该方案的优点和不足。

计算机图形学课程的教学研究

计算机图形学是计算机学科一门重要的专业课程，它主要研究各种几何和自然形体如何由计算机自动生成、显示、存储等的一门学科。笔者主持了计算机图形学的精品课程和网络课程的建设。在对这门课多年的本科教学实践过程中，通过深入了解、观察和体会，在结合国内外一些知名大学的教学经验的基础上，对该课程的授课方式、实验内容和方式等教学环节方面总结出了一些切合实际的经验和方法。

文语转换显示系统中多线程技术的应用

论文介绍如何把多线程技术较好应用在文语转换显示系统中。通过介绍多线程技术中的一些关键问题和文语转换显示系统的一些特点,设计了对文语转换显示系统中比较适合的多线程的构架。

有界模型检测和串空间模型相结合的安全协议验证

提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,进行验证,有效减轻状态空间爆炸问题;利用不安全协议丛结构的特点,对BMC的下界进行优化.这种方式结合了模型检测和定理证明的优点,通过典型的安全协议的分析和实验,验证了本方法较传统的模型检测方法在验证安全协议时,验证效率提高明显.

计算机图形学课程群的教学改革与建设

计算机图形学课程群是高校计算机专业的核心课程群。根据该课程群教学特点及课程间相互的内在关系,进行课程群的教学内容、教学模式、教学团队、网络教学资源等方面的建设。通过该课程群的建设提高教学质量、优化教学资源,使不同计算机方向的学生高效适合的获取该课程群的课程知识。

部件轮廓汉字的自动生成

本文提出运用图形学中布尔运算的方法对笔划轮廓汉字进行自动处理而生成部件轮廓汉字 ,并对传统的布尔运算中的重合线段的跟踪、特殊交点的处理进行有效的改进 .以此为基础在微机上开发了部件轮廓汉字自动生成系统 ,可高效生成标准、规范 ,成本低的部件汉字 ,具有较大的应用价值 ,本文叙述汉字的布尔模型、部件汉字生成的实现算法等 .

电子商务中安全协议的验证方法

该文简述了电子商务中的安全协议验证技术,对目前的一些重要的研究方法进行了分析和比较,重点针对形式化的方法在电子商务中的安全协议验证中的优势和不足,结合实际,提出了一些可能的发展趋势。

对辐射度光照模型的改进

本文简述辐射度方法的光照模型，对该光照模型中的形状因子的求解和辐射度方程的求解在方法上进行了有效的改进，通过实验证明所做的改进是成功的．