基于纹理语义特征的图像检索研究

针对Tamura纹理模型,提出了基于语言变量的图像纹理语义特征描述方法;并通过遗传程序设计构造从低层视觉特征到高层语义特征的映射;最后根据这些模糊语义值进行图像检索．实验结果表明系统不仅能得到出众的检索效率,而且与人类的视知觉具有比较好的一致性,提出的方法对于缩小低层视觉特征和高层语义特征之间的“语义鸿沟”具有很大的意义．     

视频数据库的聚类索引方法

理想的视频库组织方法应该把语义相关并且特征相似的视频的特征向量相邻存储.针对大规模视频库的特点,在语义监督下基于低层视觉特征对视频库进行层次聚类划分,当一个聚类中只包含一个语义类别的视频时,为这个聚类建立索引项,每个聚类所包含的原始特征数据在磁盘上连续存储.统计低层特征和高层特征的概率联系,构造Bayes分类器.查询时对用户的查询范例,首先确定最可能的候选聚类,然后在候选聚类范围内查询相似视频片段.实验结果表明,文中的方法不仅提高了检索速度而且提高了检索的语义敏感度.     

基于纹理谱描述子的图像检索

提出一种新的纹理谱描述子应用于基于内容的图像检索中.讨论了小波变换的思想和纹理谱概念的联系,根据纹理的视觉特性,提出纹理模式等价类的概念,设计出更合理的纹理谱描述子来描述图像的纹理特征.该纹理模式刻画了领域内像素灰度变化模式,以纹理谱直方图方式表示图像纹理内容.分析了纹理谱的对称不变性和旋转鲁棒性的特点.应用于图像检索,与G曲or纹理特征相比较,该纹理谱描述子特征提取速度快,检索准确率高.     

集成视觉特征和语义信息的相关反馈方法

为了有效地利用图像检索系统的语义分类信息和视觉特征,提出一种基于Bayes的集成视觉特征和语义信息的相关反馈检索方法.首先,将图像库的数据经语义监督的视觉特征聚类算法划分为小的聚类,每个聚类内数据的视觉特征相似并且语义类别相同;然后以聚类为单位标注正负反馈的实例,这显著区别于以单个图像为单位的相关反馈过程;最后分别以基于视觉特征的Bayes分类器和基于语义的Bayes分类器修正相似距离.在图像库上的实验表明,只用较少的反馈次数就可以达到较高的检索准确率.     

函数矩阵及其微积分的高阶逻辑形式化

函数矩阵广泛应用于动态系统的建模与分析。传统的函数矩阵分析主要采用纸笔演算、数值计算和符号推导的方法,这些方法不能保证提供精确或正确的结果。高阶逻辑定理证明作为一种高可靠的形式化验证方法,可以克服以上不足。在高阶逻辑定理证明器HOL4中对函数向量和函数矩阵相关理论进行形式化,内容包括函数向量和函数矩阵及其连续性、微分、积分的形式化定义和相关性质的逻辑推理证明。为示范函数矩阵形式化的应用,最后给出机器人运动学中旋转矩阵微分公式的形式化验证。     

几何代数的高阶逻辑形式化

几何代数是一种用于描述和计算几何问题的代数语言.由于它统一的表达分析和不依赖于坐标的几何计算等优点现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具, 然而利用几何代数进行计算和建模分析的传统方法,如数值计算方法和符号方法等都存在计算不精确或者不完备等问题.高阶逻辑定理证明是验证系统正确的一种严密的形式化方法.本文在高阶逻辑证明工具HOL-Light中建立了几何代数系统的形式化模型,主要包括片积、多重矢量、外积、内积、几何积、几何逆、对偶、基矢量运算和变换算子等的形式化定义和相关性质定理的证明.最后为了说明几何代数形式化的有效性和实用性,本文在共形几何代数空间中对刚体运动问题提供了一种新的简单有效的形式化建模与验证方法.     

运用定理证明的形式化方法验证SpaceWire编码电路

我国空间太阳望远镜(SST)项目采用了SpaceWire作为传输总线,目前针对SpaceWire总线的验证主要采用测试和模拟等传统的方法,这类验证方法是不完备的.本文旨在对SST项目中SpaceWire总线的DS编码电路是否如实地实现标准中的规范要求进行验证,运用定理证明的形式化方法,在HOL4工具上对该电路的设计实现与规范要求的一致性进行验证,克服了传统验证方法的局限性.     

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑，操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障，造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生，对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误，因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中，互斥量可协调多任务对资源的访问，是一种常用的任务同步方式，其功能正确性对于保障多任务应用的正确性十分关键.本文基于定理证明方法，在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模，给出其接口函数的形式化规范，并实现这些接口函数的功能正确性验证.     

实时嵌入式双操作系统架构研究综述

随着全球工业4.0战略的提出,工业控制及航空航天等领域对嵌入式系统的要求越来越高,对实时性具有严格要求同时还需要应用功能丰富的通用操作系统的支持.针对该需求现状,学术界和产业界提出双操作系统的解决思路,即同时运行实时操作系统和通用操作系统.本文归纳总结国内外嵌入式双操作系统的研究现状,对各种实现技术进行深入探讨和分析,列举嵌入式双操作系统典型应用和主要应用领域,最后对该类技术的研究趋势进行总结.     

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.