一种ROS底层通讯机制的形式化建模与验证方法及其应用

摘要

本发明公开了一种ROS底层通讯机制的形式化建模与验证方法，首先根据ROS的开源代码，提取出来ROS底层通讯机制的模块、功能和规则；建立其关于底层主题通信机制的形式化模型；根据“发布/订阅”通讯机制，提取出关键性质，用时态逻辑语言来描述性质；设计ROS应用实例，使用形式化验证工具，通过结合应用实例和所建立的形式化模型，对时态逻辑语言描述的关键性质进行验证；根据验证结果和过程，对ROS的“发布/订阅”通讯机制进行分析。本发明应用到包含了三个互相订阅的节点的ROS具体实现，通过形式化验证，来提高ROS及ROS应用实现的无死锁性、可达性、活性与正确性。