机器人形式化验证方法综述  

Method for Formal Verification of Robot

作　　者：刘永梅[1] Liu Yongmei(Beijing Key Laboratory of Light Industrial Robots and Safety Verification,Capital Normal University,Beijing 100048,China)

机构地区：[1]轻型工业机器人与安全验证北京市重点实验室首都师范大学信息工程学院

出　　处：《信息记录材料》2019年第12期1-4,共4页Information Recording Materials

基　　金：国家自然科学基金项目面向机器人的几何代数高阶逻辑形式化理论(61572331)资助

摘　　要：机器人的形式化验证方法通常很复杂,目前还没有一种通用的方法。本文对机器人的形式化设计和验证的概念进行介绍,描述其框架和基本方法。调查多个设计和验证项目,阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上,分析和展望机器人形式化设计和验证的发展趋势,从机器人模型设计、验证工具、代码实现等方面给出形式化设计和验证的思路。The formal verification of robot is usually a complex task.At present,there does not exist a general methodology for verifying robot systems.This paper introduces the concepts of formal design and verification for the robot,and elaborates the framework and foundational methods of formal design and verification.It investigates multiple design and verification projects in depth,focusing on the verification objectives,the methodology,the advantages and limitations,and the progression.It analyzes and outlooks the trends of the formal design and verification for the robot.What is more,from the aspects of model design,verification tools,and code implementation,it advances the ideas of formal design and verification.

关 键 词：机器人 形式化设计 形式化验证 定理证明 模型检验 

分 类 号：TP24[自动化与计算机技术—检测技术与自动化装置]