形式模型驱动的人机协作机器人设计与验证方法研究

The robot is a comprehensive system which integrates motion control, environmental perception, trajectory planning, target recognition and knowledge reasoning. It involves many subjects, such as machinery, electronics, computer science, automatic control and so on. The human-computer cooperative robot system usually requires high reliability and safety. Therefore, how to improve the reliability and safety of the robot system is a major challenge. In order to build a safe and reliable robot control system, this project explores the formal model driven design and development method under the domain knowledge constraints. 1. We proposes the component modeling method and the domain component library of the human- cooperative robot. 2. A code generation method based on the established time automata model is proposed. 3. In the complex environment of the robot, the run time verification technology ensures that the control program parameter can be automatically adjusted according to the changes of the environment parameters. The above contents form a common framework for the high credibility and safety development of the robot. Finally, modeling tool, automatic code generation tool and run time verification tools will be implemented and applied to a human cooperative robot.

机器人是集运动控制、环境感知、轨迹规划、目标识别、知识推理等于一体的综合性系统，涉及机械、电子、计算机、自动控制等多门学科。人机协作机器人系统通常是安全攸关系统，对系统的安全性和可靠性有着极高的要求。因此，如何提高机器人系统的可靠性和安全性是当前研究的一大挑战。本课题以构建安全可靠的机器人控制系统为出发点，探索在领域知识约束下的形式模型驱动的设计与开发方法。主要研究点包括：1.提出人机协作机器人构件化建模方法和领域构件库。2.提出基于时间自动机模型的机器人控制代码自动生成方法。 3.在机器人运行的复杂环境中，通过运行时验证技术确保能够根据环境因素的变化自动调节控制程序参数。上述内容共同组成了机器人高可信安全开发框架。最后，实现建模工具原型，代码自动生成工具，运行时验证工具。选择一种人机协作机器人，完成它的开发和运行维护。

机器人的应用越来越广泛，不同于软件，机器人是软件控制的机械机构，微小错误就会造成人身危险。因此，人机协作机器人系统通常是安全攸关系统，对系统的安全性和可靠性有着极高的要求。本课题以构建安全可靠的机器人控制软件为出发点，研究形式模型驱动的机器人软件设计与开发方法。主要研究内容包括：模型层，构建模型组件库、设计组件连接方式，重点解决了复杂机器人系统软件和硬件协同建模问题；设计实现基于转换的模型验证方法，能够验证混合模型的正确性。提出基于形式模型的机器人控制代码自动生成方法，并实现了相关工具，大大简化了开发的时间，提高了程序的正确性。代码层，提出了基于模糊测试的ROS软件包漏洞检测方法，找到了软件中存在的内存泄漏、数组访问越界和段错误等多个漏洞，并得到了软件开发者的确认，该工具适用于大多数的ROS软件包的测试。在机器人运行的复杂环境中，提出了面向关键属性的实时数据在线监控方法，通过运行时验证技术，确保能够根据环境因素的变化自动调节控制程序参数。