随着人工智能、机器人技术的不断发展和变革,机器人正逐渐进入人类生产生活的各个领域,机器人操作系统（Robot Operating System,ROS）因此得到广泛的应用并受到学术界和产业界的共同关注。其中,ROS安全测试与验证成为机器人操作系统研究领域的热点问题之一。通信机制作为ROS最基础的功能,在保证系统的正确性和安全性方面具有不可替代的作用。进一步说,ROS安全不仅应当从仿真和测试出发来进行验证,同时还必须通过形式化方法来保证安全验证的完备性。所以,本文将从形式化验证的角度出发,通过分析ROS系统源码,提取相关通信机制也即基于话题、服务、动作等三种通信机制的实现方案,进而建立相应的形式化模型,并利用UPPAAL验证相关通信机制的安全可靠。本文主要工作及贡献如下:首先,概要分析了ROS的全部源码,从中提取和确立了ROS实现上述三种通信机制的核心源码范围。在此基础上,研究给出了每一种通信机制的类图。针对话题型通信机制,具体讨论分析了发布者类和订阅者类各自的功能实现、彼此间的关系以及（发布者）消息发布流程、（订阅者）消息订阅流程;针对服务型通信机制,具体讨论分析了服务器类和客户端类各自的功能实现、彼此间的关系以及（客户端）请求消息流程、（服务器）响应消息流程;针对动作型通信机制,具体讨论分析了服务器类和客户端类各自的功能实现、任务状态机以及（服务器）Simple调度策略和（客户端）任务取消策略的实现。然后,在研究UPPAAL模型构建模式及源码抽象原则基础之上,针对ROS通信机制提出了形式化建模和验证的技术路线,根据前面基于源码的ROS三种通信机制分析结果,分别建立了相应的UPPAAL形式化模型。针对话题型通信机制,具体就发布者和订阅者的队列溢出及通信机制死锁等安全属性分别展开形式化验证;针对服务型通信机制,具体就通信机制的可达性和活性等安全属性分别进行形式化验证;针对动作型通信机制,具体就客户端和服务器的任务状态机的死锁,服务器的Simple调度策略的调度性、可抢占性以及任务执行的唯一性,客户端的任务取消策略的可达性逐一进行了形式化验证。上述所有验证结果均表明对应通信机制满足相应各项安全属性,进而验证了现有ROS通信机制实现的安全性和可靠性。此外,论文还设计相应的测试用例程序对上述三种通信机制分别实施了可靠性测试,进一步印证了本文形式化验证技术路线的可行性及验证结果的可信性。论文的主要创新性贡献包括基于源码分析的ROS通信机制形式化建模与安全验证技术路线的提出以及关于ROS所有三种通信机制相关安全属性形式化验证的实现。今后可就形式化验证工具的设计和实现以及基于源码的形式化模型的自动构建方法和技术展开进一步的研究。