【摘 要】
：
对机器人控制算法进行验证工作,对于保障机器人安全工作具有重要意义.本文给出了一个可以在双臂机器人无碰撞运动规划中应用的空间线段距离算法,并完成了对这个算法正确性的形式化验证.本文中的形式化验证工作在定理证明器HOL4中实现,包括基本几何定义和定理的表示和证明,基于霍尔逻辑将算法表示成待证明的目标以及对这个目标的证明.
【机 构】
：
高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室,首都师范大学信息工程学院,北京100048
论文部分内容阅读
对机器人控制算法进行验证工作,对于保障机器人安全工作具有重要意义.本文给出了一个可以在双臂机器人无碰撞运动规划中应用的空间线段距离算法,并完成了对这个算法正确性的形式化验证.本文中的形式化验证工作在定理证明器HOL4中实现,包括基本几何定义和定理的表示和证明,基于霍尔逻辑将算法表示成待证明的目标以及对这个目标的证明.
其他文献
本文主要工作集中于基于TTCN-3的协议一致性测试方法研究,介绍了TTCN-3核心语言.以DNS协议为例,在对DNS协议进行分析的基础上,结合TTCN-3测试系统的体系结构和一致性测试过程,提出了一种通过执行TTCN-3抽象测试套来验证协议实现正确性的方法.论文主要是根据TTCN-3核心语言的相关规范与DNS协议的工作方式,设计了测试DNS协议的TTCN-3抽象测试套;根据TTCN-3控制接口规范
本文介绍功率器件加速老化及故障预测实验平台的搭建方案.分析了进行功率循环、热循环、负载变化等功率器件加速老化实验所需的实验条件和要求.介绍实验平台搭建的整体框架,软件、硬件部分的组成实现.该实验平台可以在线监测器件电压Vce(Vds)、Vg、电流Ice(Ids),封装温度等,并获得器件全生命周期的老化数据,支持功率器件状态监测和故障预测方法的在线验证.
Scan-based testing always consumes considerable power as the transitions due to the shifting of test data in scan chain can cause excessive nonsense work in the combinational part of the circuit.Scan
通用处理器是集成电路中功能最为复杂的设计之一,这对其功能验证提出了巨大的挑战.本文提出了一种基于指令模板的通用处理器约束随机指令生成方法,针对一款ARMv8处理器进行了模拟验证.此指令生成方法基于从指令集中提炼的指令模板,通过约束的调整即可支持各种功能场景的验证.基于结果自动比对的验证环境,对处理器进行了充分的验证,发现了58处设计错误,为处理器进入后续的FPGA硬件仿真奠定了良好的基础.
传统扫描链将所有扫描单元串联,测试数据的移位路径较长,导致测试移位功耗较大.首次提出代表扫描结构,它将传统扫描链或子链中的触发器改造成环形移位寄存器,为每个环形移位寄存器遴选一个代表触发器,并将这些代表触发器串联,构成具有若干局部循环的代表扫描结构.本文首次提出代表扫描结构，该结构仅选择部分代表触发器串联成代表扫描链作为测试数据的移位路径，大大减少了移位功耗，该结构的不仅具有较小的硬件代价，获得较
集成电路工艺水平的不断提高,使得组合逻辑电路对软错误的敏感性越发突出.为了在集成电路的设计阶段进行软错误率的准确评估,提出一种精确的单粒子瞬态屏蔽效应评估方法.该方法考虑了扇出重汇聚的影响,考虑了门单元输入引脚到达输出端的上升与下降延迟,并克服了现有时窗屏蔽效应评估方法存在的不足.基于提出的单粒子瞬态屏蔽效应评估方法,提出一种基于向量传播的组合逻辑电路软错误率计算方法.通过将不同宽度的瞬态故障脉冲
程序的异常处理机制是提高软件可靠性与软件容错的常用重要手段之一，该机制可以将程序从错误状态恢复到正常状态，避免软件失效的发生或以安全的方式退出程序。当程序发生错误且该错误被异常处理机制侦测时,程序控制流会跳转到异常控制流中进行相关异常的处理.异常控制流的发生表明了程序正处于错误状态之中,即程序存在差错.但目前相关研究并没有从异常控制流的角度对程序的错误行为进行描述与分析.针对以上问题,本文提出了一
原始测试用例生成方法通常被认为会影响蜕变测试的有效性.ART(Adaptive Random Testing)作为一种改进的随机测试方法,在保留传统随机测试方法优势的同时,又可以克服其盲目性.基于此,论文为了提高软件蜕变测试的性能,在传统蜕变测试原始测试用例生成过程中引入ART算法,从而形成了一种基于ART的蜕变测试用例生成方法(MT-ART).通过该算法可以生成更加有效的原始测试用例,可以提高蜕
Intel提出的第三代总线技术PCI Express对计算机应用系统发展所带来的总线带宽需求有了很大的满足,基于PCIE的设计因此蓬勃发展,对PCIE的验证也因此成为SoC功能验证的重要组成部分.本文设计并实现了一种状态图和覆盖率组合驱动的验证平台,主要包括激励生成、自动检测和覆盖率分析机制,并将其应用于一款基于PCIE接口的协议栈芯片的功能验证.实验结果表明,本文实现的验证平台具有良好的激励生成
SRAM型FPGA具有设计周期短,可动态重构等特点,已在航空航天、金融电信等领域得到广泛应用.但是,随着晶体管工艺尺寸的不断减小,晶体管密度的不断提高,SRAM型FPGA的功耗问题日益突出.本文提出了一种面向重布局的SRAM型FPGA片上温度测量方法,即在片上设计环形振荡器作为温度传感器,将其与开源转商用的设计流程VTR-to-Bitstream产生的原始电路设计相结合,使得在电路运行期间可以实时