软件学报

作者：谢果君，杨焕焕，石正璞，陈钢

单位：谢果君，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110611,杨焕焕，国防科技大学 计算机学院, 湖南 长沙 41007302,石正璞，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110603,陈钢，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110604

关键词：机器人运动学;形式化验证;DH坐标系;代码自动生成

DH坐标系在机器人运动学分析中发挥着重要的作用. 在基于DH坐标系构建的机器人控制系统中, 机器人结构的复杂性使得构建安全的控制系统成为一个难题, 仅依靠人工方法可能导致系统漏洞和安全风险, 从而危及机器人的安全. 形式化方法通过演绎推理与代码抽取实现了对软硬件系统的设计、开发及验证. 基于此, 设计基于DH标定的机器人正向运动学的形式化验证框架. 在Coq中构建机器人运动理论的形式化证明, 并验证控制算法的正确性以确保机器人的运动安全. 首先, 对DH坐标系进行形式化建模, 构建相邻坐标系间转换矩阵的形式化定义, 并验证该转换矩阵与复合螺旋运动的等价性; 其次, 构建机械臂正向运动学的形式化定义, 并对机械臂运动的可分解性进行形式化验证; 再次, 对工业机器人中常见连杆结构及机器人进行形式化建模, 并完成正向运动学的形式化验证; 最后, 实现Coq到OCaml的代码抽取, 并对抽取的代码进行分析与验证.

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期