穿刺机器人运动安全性的形式化分析与建模

混成系统是实时嵌入式系统的重要子类,其行为中存在连续变化和离散跳转混杂的情况,使得混成系统行为复杂,安全性难以掌握。近年来,混成系统在医疗环境中得到越来越广泛的应用。其中,医疗机器人的穿刺运动控制系统呈现高度复杂的混成性,如果机器人在穿刺过程中失控将导致不可挽回的严重后果。因此穿刺机器人运动行为的安全性设计成为了亟需解决的问题。首先根据穿刺机器人的运动学设计,将机器人的复杂运动分解。然后基于微分动态逻辑理论从混成系统的角度出发对穿刺机器人的运动控制系统进行了形式化建模与分析,并使用证明工具KeYmaera归纳出微分不变式,获得了控制模型的参数约束。最后提出了针对机器人运动到某一靶目标区域这类运动学问题的一般性验证模型。     

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

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

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

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

融合语义主题的图像自动标注

由于语义鸿沟的存在,图像自动标注已成为一个重要课题.在概率潜语义分析的基础上,提出了一种融合语义主题的方法以进行图像的标注和检索.首先,为了更准确地建模训练数据,将每幅图像的视觉特征表示为一个视觉"词袋";然后设计一个概率模型分别从视觉模态和文本模态中捕获潜在语义主题,并提出一种自适应的不对称学习方法融合两种语义主题.对于每个图像文档,它在各个模态上的主题分布通过加权进行融合,而权值由该文档的视觉词分布的熵值来确定.于是,融合之后的概率模型适当地关联了视觉模态和文本模态的信息,因此能够很好地预测未知图像的语义标注.在一个通用的Corel图像数据集上,将提出的方法与几种前沿的图像标注方法进行了比较.实验结果表明,该方法具有更好的标注和检索性能.     

最大目标频繁模式挖掘算法研究

传统的频繁模式挖掘算法往往会得到成百上千的结果模式,面对繁多的频繁模式用户通常要经过“二次挖掘”才能得到有用的目标模式。怎样根据用户需求直接挖掘用户感兴趣的目标模式是该文的研究目标。文章在FP-树的基础上设计了紧缩的、非冗余的TFP-树,它能有效过滤与目标模式无关的项和事务,而仅保留与目标模式相关的信息,缩小TFP-树的大小规模。同时根据TFP-树的规律和特点,笔者设计了最大目标频繁模式挖掘算法,算法的结果模式具有以下两个特点:(1)满足用户需求的目标模式;(2)最大模式。该实验结果验证了TFP-树算法是有效的,而且显著改善了FP-树算法的性能。     

面向数据流的ROS2数据分发服务形式建模与分析

机器人操作系统(robot operating system,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题,ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法,分析、验证ROS2系统数据分发机制的实时性和可靠性.首...     

轻量级卷积神经网络的机器人抓取检测研究

卷积神经网络在基于视觉的机器人抓取检测任务上取得了较好的检测效果,但是大多数方法都有太多的计算参数,不适合资源有限的系统。针对这个问题,基于SqueezeNet轻量级神经网络,结合DenseNet多旁路连接加强特征复用的思想,提出了轻量级抓取检测回归模型SqueezeNet-RM（SqueezeNet Regression Model）,并使用SqueezeNet-RM从RGB-D图像中提取多模态特征,预测二指机器人夹持器的最佳抓取位姿。在标准的康奈尔抓取数据集上,提出的轻量级抓取检测网络与经典的抓取检测方法相比,在保证检测准确率不降低的情况下,模型占用更少的存储空间,表现出更快的检测速度和更高的泛化性能,所提出的模型占用的存储空间比AlexNet模型减少86.97%,平均检测速度快3倍,适用于FPGA（Field Programmable Gate Array）或者资源受限的移动机器人抓取检测系统。     

一种CBR与RBR相结合的快速预案生成系统

将范例推理(case based reasoning,CBR)与规则推理(rule based reasoning, RBR)两种人工智能技术相结合,实现一种快速预案生成系统.它有效地解决了单纯RBR系统在预案生成过程中的时间延迟缺陷和知识库难以获取的瓶颈.通过CBR工具,能够把以前发生的紧急事件和解决方案生成预案.一旦新的事件发生,首先从预案库中进行案例的相似性检索,如果没有检索到预案或者检索到的预案匹配度很低,再采用RBR系统对紧急事件进行规则推理,然后把推理结果重新存入预案库.实验数据表明,这种方法对单纯RBR系统在时间响应上进行了有效的优化.另外,因为案例的获取比专家系统推理规则的获取容易得多,它同时解决了RBR系统推理规则难以获取的瓶颈.根据这种思想,实现了CBR与RBR结合的快速预案生成系统.目前,它已经应用到抗洪抢险的预案生成和城市应急联动的决策支持上,效果表明它在预案生成速度以及实际可操作性上都具有明显优势.     

建模连续视觉特征的图像语义标注方法

针对图像检索中存在的"语义鸿沟"问题,提出一种对连续视觉特征直接建模的图像自动标注方法.首先对概率潜语义分析(PLSA)模型进行改进,使之能处理连续量,并推导对应的期望最大化算法来确定模型参数;然后根据不同模态数据各自的特点,提出一个对不同模态数据分别处理的图像语义标注模型,该模型使用连续PLSA建模视觉特征,使用标准PLSA建模文本关键词,并通过不对称的学习方法学习2种模态之间的关联,从而能较好地对未知图像进行标注.通过在一个包含5000幅图像的标准Corel数据集中进行实验,并与几种典型的图像标注方法进行比较的结果表明,文中方法具有更高的精度和更好的效果.     

连续傅里叶变换基础理论的高阶逻辑形式化

连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用.利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相关系统奠定了基础.最后利用定理证明的方法对电阻电感电容(RLC)串联谐振电路的频率响应特性进行了验证,说明了CFT形式化的初步应用.