基于可信执行环境的机器人实时操作系统架构及形式化验证研究

操作系统是机器人控制器的关键组成部分，它对于碰撞检测、紧急制动等实时控制功能和运动规划、图像处理等复杂计算功能的实现具有重要作用。单一的实时操作系统不满足机器人控制对复杂计算功能的要求；现有双操作系统架构不能有效保证实时和通用操作系统故障隔离，且未经过严格的形式化验证，不满足机器人控制系统对可靠性的要求。本项目将采用基于硬件隔离机制建立可信执行环境的方式构建双操作系统架构，并利用形式化验证技术分析架构可靠性，重点研究基于可信执行环境的机器人实时操作系统架构，以及基于标记转换系统分析该操作系统架构隔离、调度和通信等核心机制的形式化验证方法，实现满足实时控制、复杂计算、形式化验证要求的机器人实时操作系统架构，支持机器人软件的模块化开发和分布式运行，为机器人操作系统设计和应用提供技术支撑，并为机器人控制软件形式化验证奠定理论基础，对机器人控制技术发展和推广具有重要意义。

The operating system is a critical component of the robot controller, which plays an important role in the implementation of collision detection, emergency braking or other real-time control functionalities and motion planning, image processing or other complex computation functionalities. The real-time operating system can not meet complex computation requirements of robot control. The existing dual operating system (dual-OS) architectures can not effectively guarantee the fault isolation between the real-time operating system and the general purpose operating system, and they do not undergo rigorously formal verification, which makes them not meet the reliability requirement of the robot controller. This project will build a dual-OS architecture by establishing a trusted execution environment (TEE) using hardware-based isolation mechanisms, and will carry out the formal verification of the architecture to analyze its reliability. We focus on the research of building the TEE-based robot real-time operating system architecture, and the formal verification method which is based on the labelled transition system to analyze the core mechanisms (isolation, schedule, and communication) of the operating system architecture. The goal of the project is to present a robot real-time operating system architecture, which meets requirements of real-time control, complex computation, and formal verification, and supports the modular development and distributed execution of robot software. This research will provide strong technical support for the design and application of robot operating systems, and will build theoretical basis for the formal verification of robot control software, so this research is important for the development and promotion of robot control technology.