摘要:模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术，并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用，并且随着各种状态空间简化技术和模型检测算法的不断优化，其在其他应用领域也展示出广泛的应用前景.

摘要:上下文无关语言上递归函数(recursive functions on context-free languages,简称CFRF)是为描述计算机上用的非数值算法而提出的一种新型递归函数.该函数的一个重要研究方面是函数的求值算法研究.对此问题的一些研究结果进行了总结.在讨论计算和语法分析的结合方式之后,对主要算法按照算法适用范围从小到大的顺序(同时也是算法研究和提出的顺序)做了较为全面的介绍,着重介绍一种通用的新的高效求值算法,即面向树的求值算法.同时对把CFRF扩充为多种类递归函数后的求值方法进行了说明.CFRF的几个求值算法均已在机器上实现,得到了实践的检验.

摘要:针对如何从现存的系统中提取构件的问题,提出了一种基于有向带权图迭代分析的面向对象系统分解方法.它将面向对象系统抽象为一个有向带权图,使用迭代算法考察不同粒度的子图的独立性,并选择独立性高的作为候选构件.实验结果表明,该方法是一种有效的系统分解方法,在准确性上比现有系统分解方法有所提高.

摘要:由于形式规格说明采用一种精确、一致、容易被机器自动处理的符号系统来描述软件需求,因而形式规格说明为测试用例的自动生成和软件功能的验证提供了基础.在基于形式规格说明的测试过程中逻辑覆盖测试准则是一组常用的测试准则,如何选择和使用其中的每个测试准则是应用这组测试准则时面临的主要问题.因此分析和比较这组测试准则中每个测试准则的性质将为测试工程师选择测试准则提供指导和帮助.对测试充分性准则的公理化评估是一种比较测试准则的方式,这种方式将对理想的测试准则的直觉需求定义为一组公理,然后通过检查测试准则是否满足该组公理来分析和比较相应的测试准则.描述了一组理想的逻辑覆盖测试准则应该具有的性质和用来确定一个测试充分性准则是否完全的生成算法.这组性质被形式化地定义为一组公理.利用这种形式化的定义,用定理的形式精确地给出了这些性质之间的关系.最后通过这组公理系统来评估现有的逻辑覆盖测试准则.评估的结果为测试人员在实际过程中选择逻辑覆盖测试准则提供了指导.

摘要:计算与数据划分问题是影响并行程序在分布主存多处理机中执行性能的重要因素,也是并行编译优化的重点.针对该问题,提出了一套关于数据空间融合的理论框架,并基于该框架给出了一种有效的全局计算与数据划分方法,用于分布主存计算环境中的计算与数据划分问题的求解.该方法能够尽量开发计算空间的并行度,利用数据融合技术优化数据分布,并能搜寻优化的全局计算与数据划分.该方法还能很自然地与数据复制以及偏移常量的对准结合在一起,从而使得数据通信量尽可能地小.实验结果表明了所提出方法的有效性.

摘要:多示例学习为中文Web挖掘提供了一种新的思路.提出中文Web目录页面推荐这种特殊的Web挖掘任务,并且将其转化为多示例学习问题来解决.在真实世界数据集上的实验结果显示,该方法能够有效地解决该问题.

摘要:相关反馈技术是基于内容图像检索研究的一个重要组成部分.近年来,人们对相关反馈算法开展了许多研究工作,并提出了多种算法.目前,多数的相关反馈算法都是基于二值的相关度量--相关或不相关.为了更好地辨别用户的需要和偏好,就需要考虑相关性在程度上的差异而采用更精细的度量尺度.探讨了支持多级相关度量的相关反馈问题,指出相关反馈问题可以看成是一个顺序回归问题,并讨论了它的特点和损失函数.基于一个顺序回归的支持向量学习算法,提出了一种新的相关反馈方案.由于传统的检索性能度量(比如查准率和查全率)不适合多级相关度量的情况,采用了一种建立在图像间偏好关系上的检索性能度量.在现实世界图像数据库上的实验结果验证了所提出相关反馈方法的有效性.

摘要:基于模型的诊断方法是人工智能领域发展起来的一个十分活跃的分支.在该方法中,由极小冲突集求解极小击中集的过程是一个NP-Hard问题.尽管人们提出了不少算法,但是各种算法的效率仍然不是十分理想.通过将该问题映射到0/1整数规划问题,提出了将遗传算法与模拟退火算法相结合的问题求解思想.在给出遗传模拟退火(genetic simulated anncaling,简称GSA)算法和算法各个参数的同时,对算法的性能和求解精度进行了测试.GSA算法不仅比传统的算法效率有很大的提高,而且在冲突集基数大于35的情况下,较单独使用GA的算法在效率上提高约1/3～1/2.在求解精度上,GSA算法在大多数情况下能够求出98%～100%的极小诊断.

摘要:在移动通信网络环境中,如何合理地组织和存储移动对象的配置信息,从而有效地降低查询和更新代价是位置管理中的一个重要问题.将数据挖掘应用到移动计算环境中是一项具有挑战性的研究课题,具有广阔的应用前景.区域划分能够优化位置数据库的拓扑结构,有效地降低查询和更新代价.但是随着时间的迁移,用户的移动模式会发生改变,导致原有区域的划分与当前的移动模式不符,因此产生了动态区域划分这一亟待解决的重要问题.聚类可以很好地解决区域划分问题,而对于动态区域划分问题,如果仍然采用聚类来解决,就等于重新划分,没有充分利用原有划分的信息,所需代价很大.提出了一种增量的聚类算法来解决动态区域划分问题.该方法以较小的代价调整原有划分,使得新得到的划分仍然满足区域划分所需满足的条件.

摘要:索引技术是基于内容的相似性检索的核心内容,而数据的分割则是影响索引性能的关键因素.提出一种高维数据空间分割策略--在距离分割基础上基于关键维的二次分割,以及相应的索引技术.基于关键维的二次分割保证孪生兄弟节点的无重叠性,而在索引中根据选定的关键维进行孪生兄弟节点间的二次过滤,从而增强过滤效率.这种数据分片策略和索引技术使得索引的过滤效率成倍提高.实验结果显示,关键维能够很好地提高索引的相似性检索性能,对于加速基于内容的多媒体信息检索具有很大的意义.

摘要:介绍了对等计算(peer-to-peer,简称P2P)的特征、潜在优势和应用范围,指出了当前P2P数据共享系统存在仅支持弱语义(甚至缺乏语义)和粗粒度(文件水平)共享等局限性.针对这种现状,提出了基于P2P的信息检索,既可充分发掘P2P技术的潜在优势,克服传统信息检索系统的可伸缩瓶颈等问题,又可实现P2P数据共享系统语义丰富和细粒度的信息检索与共享;并开发出PeerIS:基于P2P的信息检索系统.描述了PeerIS的整体构架与节点的内部结构;重点阐述了PeerIS的通信机制、自配置机制、查询机制以及自适应路由机制等实现关键技术;并用实验证明了PeerIS的优异性.

摘要:安胜安全操作系统是自主研制的基于Linux的高安全等级安全操作系统,包括安全内核,安全架构与安全模型.总结了对该系统进行的隐蔽通道分析方法,首次报道基于Linux内核开发的安全操作系统的隐蔽通道分析结果.应用新型的"回溯方法"发现了某些新的隐蔽通道.对被标识的隐蔽通道,准确地计算了它们的带宽,并进行了适当的隐蔽通道处理.

摘要:随着Web所拥有的信息量和信息种类的急剧增长,Web站点挖掘对于自动实现特定主题的Web资源发现和分类具有重要的意义.然而现有的Web站点分类或挖掘算法在利用上下文语义信息、去除噪声信息以进一步提高分类准确率等方面还缺乏深入研究.从站点的采样尺寸、分析粒度和描述结构3个方面分析了设计高效的Web站点挖掘算法所需要解决的问题.在此基础上,提出了一种新的Web站点多粒度树描述模型,并描述了包括基于隐Markov树的两阶段分类算法、粒度间上下文融合算法、两阶段去噪程序以及基于熵的动态剪枝策略在内的多粒度Web站点挖掘算法.站点的多粒度描述方法及挖掘算法为多站点查询优化、Web效用挖掘等的深入研究奠定了基础.实验表明,该算法相对于基线系统平均可以提高16%的分类准确率,并减少了34.5%的处理时间.

摘要:网络视频应用经常会受到数据包丢失或错误以及网络带宽资源不足的干扰.相关研究表明:在多数情况下,动态变化的网络带宽和丢包率是影响视频流化质量的关键因素.因此,为了保证视频质量,可以采用前向纠错(forward error correction,简称FEC)编码来提高视频数据传输的可靠性;同时,为了适应网络状态的变化,发送端可以调节视频数据的发送速率,并在视频源数据与FEC数据之间合理分配网络传输带宽.首先通过对视频流结构的分析,在充分考虑帧之间的依赖关系和帧类型的基础上提出了一种帧的解码模型.在此基础上,建立了用于在视频源数据和FEC数据之间分配网络带宽资源的优化算法.实验表明,该模型可以有效地适应网络状态的变化,并通过优化分配网络带宽资源来使接收端获得最大的可播放帧率.

摘要:稳健性是数字水印的重要指标之一.为了改善水印稳健性,一些学者在水印算法中引入了纠错编码(error correcting coding,简称ECC),试图通过纠正水印误码来降低检测误码率.然而,水印信道与一般的通信信道不同,受水印不可察觉性的限制,纠错编码中引入的信息冗余将导致水印嵌入强度的降低.换言之,纠错码的码率会极大地影响到嵌入信号的幅度.由此将引出一个问题:从改善水印稳健性的角度出发,纠错编码的码率应该如何选择?从分析和实验两个方面探讨了这个问题.给出了P1otkin限和Hamming限情况下,水印中的Q进制线性分组码应该满足的码率约束条件,并通过仿真实验检验了给出的条件.