当前,全球化“工业4.0”革命进程和我国的“中国制造2025”战略计划中,机器人均作为核心技术受到了前所未有的重视。以美国为例,谷歌公司的无人驾驶汽车、多足仿人机器人,亚马逊公司的仓储自动导引车,以及美国太空总署的好奇号火星车等都在吸引着全球媒体的目光。欧洲、日本和中国等也纷纷出台了自己的机器人研究计划。面对机器人系统及其集群任务复杂而多变的安全性需求以及恶劣与不确定性外部环境,如何安全地控制各个分布式机器人节点在外部环境下完成任务是一项严峻而又急迫的挑战性问题。在传统方法上,设计者将其设计的控制器实现并且部署到多机器人系统上对系统进行控制,这个流程是繁琐且非常容易出错的。所设计的控制器也极难保证该系统安全稳定地完成给定任务。随着近年来形式化方法理论和技术的突破,基于形式化方法的机器人系统安全性质验证已经得到了很多研究者的深入研究。想要系统性地验证和保障机器人系统及其集群系统的安全性,基于形式化方法的运行时监控是一项必要且有效的手段,能够有效提升“系统的可信度”,也是目前学界研究的热点。在众多的软硬件系统监控方法中,运行时验证（Runtime Verification,简称RV）是近年来兴起的轻量级的软件可靠性保障技术,它基于目标系统的运行轨迹来判定给定的性质规约是否满足。由于系统运行轨迹的唯一性,它有效地克服了当系统足够复杂后带来的模型检验技术的状态空间爆炸和测试技术的全路径难以覆盖的问题。另外与传统的软件可靠性保障技术不同的是,RV技术主要应用在系统部署后,对运行环境和上下文不确定导致的系统缺陷能很好地进行监控。然而,由于机器人系统的复杂性和RV技术中形式化理论的学习门槛较高,当前,RV技术在机器人集群系统上的研究还处于初级阶段,相关的应用较少。因此,本文主要研究如何把运行时验证方法应用于不确定性环境下的机器人系统,并在此基础上,研究针对机器人系统运行时性质违背的强制防护方法,具体工作和创新点包括:1)通过对基于ROS（Robot Operating System）系统的机器人特点及安全挑战的分析,本文以保障机器人导航、避障等自主行为以及集群协同控制在运行时状态下始终满足安全规约为目标,针对ROS机器人系统及其集群系统提出了领域内适用的运行时验证框架RMo M以及运行时强制防护方法。进一步丰富了基于ROS通信机理的机器人及集群系统监控和防护理论。2)当前,面向机器人系统的RV方法较少考虑混成属性和集群属性的监控,本文在MTL（Metric Temporal Logic）时序逻辑语言的基础上,针对有限序列和预测监控需求做了三值语义扩展,并首次加入了包含集群命题和算子且对机器人集群领域适应性较高的时序逻辑语言MTL3-RMo M,基于此逻辑语言能够表达并监控机器人集群系统中的集群性质、时间区间性质等。3)ROS系统下的机器人集群的RV技术应用需要基于机器人系统的全局及局部约束,涉及到各类事件和状态。本文方法实现了自定义且高可扩展的ROS机器人集群系统事件和状态接口库,基于RMo M框架提出了一种针对机器人集群的层次化性质的监控方法,该方法目前在应用中已经能够覆盖集群性质、单机器人性质、硬件资源和通信层性质的复合性质运行时验证。4)我们针对机器人系统性质违背开展了防护方法的研究,提出了一种宏/微观两级的运行时强制机制并创新性地提出了D-time强制器生成方式。这种强制方式可以在周期性的时间间隔中灵活工作,并且不需要下一个运行时环境状态的知识。本文在一个机器人集群模拟工具robotflocksim上实现和部署了这种运行时强制器生成算法,通过实验测试了该方法带来的安全性改进和开销问题。