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

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

协作机器人逆运动学形式化建模与验证

在机器人迅速发展的时代,人机协作型机器人安全性问题是人们关注的焦点.机器人逆运动学的建模与求解是决定其安全性的必要因素之一.旋量法是一种机器人逆运动学建模的常用方法,它可以解决传统D-H参数法的奇异性问题.然而,在建模过程中,旋量法会因人为因素或软件系统缺陷导致模型出现漏洞,从而威胁操作人员安全.因此,本文在旋量高阶逻...     

基于HOL4的形式化方法

针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质.     

机器人控制系统关键模块的形式化验证

随着机器人应用在越来越多的领域,人们对其安全性的要求越来越高,作为机器人的核心,控制系统设计的可靠性对整个系统的安全至关重要;针对一种模块化设计的机器人控制系统架构,利用xMAS(eXecutable MicroArchitecture Specification,可执行微架构描述)模型在定理证明器ACL2中对其功能正确性进行验证,首先对Xmas在ACL2中的形式化理论做了阐述,然后对该机器人控制系统中的加速度传感器数据采集模块建立xMAS模型,提取关键属性并进行验证;将xMAS模型和定理证明器ACL2相结合,可以很好地解决机器人控制系统的验证问题,为机器人控制系统的形式化验证提供一个有效的方法参考。     

安全协议认证的形式化方法研究

安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。     

一种水下群机器人路径规划算法的形式化研究

为了增强基于遗传算法的水下群机器人路径规划算法正确性的说服力,使用定理证明对其进行形式化研究,给出算法在定理证明器HOL4中的形式化模型。基于算法形式化的一般步骤,首先对算法的设计进行了详细的分析,指出算法设计的核心步骤与建模难点。在此基础上建立了总体形式化建模框架,然后对其进行化简,得到种群初始化、选择、交叉三个核心模块。接着给出模型中要用到的基本数据类型的形式化描述,并分别对三个模块进行形式化描述,最终得到算法的形式化模型。通过证明与模型相关的97条性质,说明了模型的合理性及有效性,在此模型的基础上,可以完成对算法的形式化验证,同时还能拓展HOL4的应用范围。     

GJK算法的一种特殊情形的形式化验证和应用

计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.     

混成系统形式化验证

混成系统是实时嵌入式系统的一种重要子类,其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况,因此行为复杂,难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域,因此,如何对相关系统进行有效的分析与理解,从而保障系统安全运营,是一项具有重要意义的工作.常规的系统安全性分析手段,如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为,无法穷尽地检测复杂混成系统在所有可能输入下的行为,因此并不足以保证系统的安全性.区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此,其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上,针对现阶段实时嵌入式系统复杂化、网络化的特性,对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.     

装配机器人系统快速碰撞检测算法

提出一种面向操作手段装配系统的快速碰撞检测算法。该算法以机器人运动学和空间解析几何为基础,将判断机械手手臂与障碍物是否发生碰撞问题转化为直线段与有界平面是否存在公共点的简单解析几何问题,并以PUMA560操作手为例对算法加以说明,该算法不仅适用于静态的障碍物已知的环境,而且适用于障碍物运动规律已知的动态环境,减少了碰撞检测占用的时间,提高了路径规划的效率。     

多机器人体间动态碰撞检测方法仿真研究

当前多结合包围求碰撞检测法、Average-Case法、K-DOPs法等实现多机器人体间动态碰撞的检测,均存在寻优性能较差、检测效率较低的问题。为此提出一种基于动态粒子群的多机器人体间动态碰撞检测方法。采用OBB层次包围盒方法,缩小多机器人之间需要动态碰撞检测的区域,同时把动态碰撞检测问题转换为物体特征对间距离机制的非线性优化问题,进而构建层次拓扑框架进行局部碰撞检测,将机器人体引入到粒子群算法中建立混合进化算法,找到动态碰撞检测的最优解,实现多机器人体间动态碰撞检测。仿真结果证明,所提方法的检测效率高达96%,且具有较高的寻优性能。     

机器人带未知负载条件下的碰撞检测算法

未知负载会增大机器人模型误差,对碰撞检测产生严重干扰,甚至导致算法失效.为此,本文提出了一种适用于机器人带负载工作情况的碰撞检测算法.首先,基于机器人广义动量设计具有带通滤波特性的新型力矩观测器,通过对机器人动力学频域特性进行分析,得到机器人动力学模型与关节运行速度对应的最大频率阈值,确定带通力矩观测器的参数.然后,利用带通力矩观测器对关节力矩信号进行滤波,提高碰撞检测算法对机器人模型误差的容忍度.最后,通过人与机器人交互实验进一步验证了该碰撞检测算法的有效性.实验结果表明,该算法与已有的算法相比具有更好的鲁棒性,可满足机器人带未知负载0～2 kg的工作需求.     

车辆碰撞事件与碰撞损伤的检测方法

提出了一种针对车辆碰撞事件的远程检测方法. 该方法利用机器学习技术分析车辆的速度和加速度信号, 从而对车辆的行驶状态进行在线监测. 车载的前端设备实时的采集速度和加速度信号, 初步识别出可能的碰撞信号并通过无线网络发送给后台服务器. 后台服务器对碰撞信号进行准确识别, 并判断车辆的损伤程度. 论文给出了碰撞事件和碰撞损伤的检测方法, 并进行了实验测试, 结果表明该方法是有效的.     

基于包围盒法的碰撞检测算法研究

随着计算机技术的日益更新,虚拟技术中的碰撞检测算法得到了快速发展。已成为国内外的研究热点。在分析了碰撞检测算法的基本理论的基础上,提出了对AABB包围盒算法的改进思想。改进后的测试结果显示测试效率提高了21．7％,证明了改进后的检测算法在检测效率上的优越性。     

基于Coq的分块矩阵运算的形式化

矩阵是工程领域中常用的一种数据结构,在深度学习领域,矩阵乘法是神经网络训练中的核心技术之一.面对大型矩阵的运算问题,分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算,并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.首先对目前学术界的矩阵形式化工作进行了系统总结,并且分析了矩阵形式化的主要几种方法;其次介绍并...     

Collision Detection for Deformable Objects

Interactive environments for dynamically deforming objects play an important role in surgery simulation and entertainment technology. These environments require fast deformable models and very efficient collision handling techniques. While collision detection for rigid bodies is well investigated, collision detection for deformable objects introduces additional challenging problems. This paper focuses on these aspects and summarizes recent research in the area of deformable collision detection. Various approaches based on bounding volume hierarchies, distance fields and spatial partitioning are discussed. In addition, image‐space techniques and stochastic methods are considered. Applications in cloth modeling and surgical simulation are presented.     

多机器人路径规划的安全性验证

近些年来,伴随着人工智能领域的浪潮,机器人越来越多的出现在我们的日常生活中,例如足球机器人、无人机、无人车等.如何保证这些自治机器人尤其是多个机器人在移动过程中的安全成了人们一直很关心的问题.混成通信顺序进程（Hybrid Communicating Sequential Process,HCSP）是一个针对混成系统的形式化建模语言,在通信顺序进程（Communicating Sequential Process,CSP）的基础上引入了微分方程以描述混成系统中的连续行为和控制逻辑,可以方便高效地对大型控制系统尤其是在有通信事件发生时的情形进行形式化建模.本文就是用HCSP建模多机器人的路径控制算法,并用定理证明工具HProver进行形式化验证.结果证明了在满足一定初始条件下,机器人团队在整个运行途中不会发生碰撞.     

一种基于可能碰撞集的碰撞检测方法

为了提高虚拟环境中碰撞检测的实时性和有效性,提出了一种基于可能碰撞集的碰撞检测方法.该方法首先通过预测环境中刚体在当前帧和下一帧之间的可能运动轨迹来构建一个各边与世界坐标系各坐标轴平行,且包围该运动轨迹的包围盒;然后利用空间平铺技术来快速检测与某一平铺单元同时相交的轨迹包围盒,即可得到当前帧的可能碰撞集;接着对可能碰撞集中的刚体对进行最早碰撞时间tmin的求解,并根据tmin进行排序;最后只对具有最小tmin值的刚体对进行碰撞检测.仿真试验结果表明,与目前已有的碰撞检测算法相比,该方法简单、快速,不仅可以有效解决多个刚体环境中碰撞发生的次序问题,同时,该方法还能保证碰撞检测的完整性和唯一性.另外,理论和实践也证明了该方法的正确性和有效性.