买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网获悉华东师范大学申请的专利针对Micro-ROS通信中间件的建模仿真与形式化验证方法及应用获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN116389281B 。

龙图腾网通过国家知识产权局官网在2025-07-04发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202211536933.3，技术领域涉及：H04L41/14；该发明授权针对Micro-ROS通信中间件的建模仿真与形式化验证方法及应用是由郭建;王子健设计研发完成，并于2022-12-02向国家知识产权局提交的专利申请。

本针对Micro-ROS通信中间件的建模仿真与形式化验证方法及应用在说明书摘要公布了：本发明公开了一种针对Micro‑ROS通信中间件的建模仿真与形式化验证方法，首先从Micro‑ROS的通信中间件MicroXRCE‑DDS的开源代码中，结合XRCE‑DDS规范，抽取出通信过程中包含的各个模块，以及各个模块的行为与功能，建立起各个模块的时间自动机模型；然后利用建模与仿真工具，对抽象的时间自动机模型进行实现，结合具体的MicroXRCE‑DDS通信应用场景，进行组合完成模型的实现和仿真；根据XRCE‑DDS规范中协议部分对通信过程的自然语言描述，抽象其中关键的重要性质，提出了一种适用于这些性质的下限为0的信号时态逻辑STLinf＝0对这些性质进行形式化表述；结合运行时验证工具，对STLinf＝0描述的关键性质进行运行时验证，根据验证结果修正模型或源码，确保模型仿真和源码的正确性和可靠性。

本发明授权针对Micro-ROS通信中间件的建模仿真与形式化验证方法及应用在权利要求书中公布了：1.一种针对Micro-ROS通信中间件的建模仿真与形式化验证方法，其特征在于，包括以下步骤： 步骤一：根据开源的MicroXRCE-DDS实现代码，提取出MicroXRCE-DDS中的MicroXRCE-DDSAgent和MicroXRCE-DDSClient所包含的行为模块，对各个模块进行基于时间自动机的形式化建模； 步骤二：基于步骤一建立的时间自动机模型，使用建模与仿真工具，结合场景应用，对MicroXRCE-DDS通信过程进行模型实现和仿真，根据仿真的结果，对模型进行修改，直至模型可以正常地进行仿真执行； 步骤三：从XRCE-DDS规范的自然语言描述中，提取通信过程需要验证的关键性质，并使用下限为0的信号时态逻辑STLinf＝0对所述关键性质进行描述；所述关键性质包括客户端到代理的可靠发送、代理到客户端的可靠发送、接收方消息的顺序接收、客户端休眠期间不被打扰、发送的消息丢失后接收方可知、丢失的消息会重新发送； 步骤四：结合运行时验证工具，在步骤二中实现的模型仿真上，进行对步骤三提出的STLinf＝0描述的关键性质进行运行时验证，并分析验证结果； 所述步骤四对关键性质在建立的模型仿真上进行形式化验证，并对验证结果进行分析，包括以下步骤： 步骤D1：基于形式化表述的STLinf＝0性质，在支持时态逻辑的运行时验证工具中表示为符合工具规则的形式； 步骤D2：根据建立的时间自动机模型，对步骤D1中的符合工具规则的性质进行运行时验证，并对验证结果进行分析； 步骤D3：如果步骤D2的验证结果存在不满足一条或多条关键性质的反例，根据反例的路径状态，找出不满足所述关键性质的时间-状态，并执行步骤D4；否则，便得到了经过形式化验证的XRCE-DDS通信机制模型仿真； 步骤D4：根据形式化验证工具中给出的反例的路径和时间-状态，分析可能的出错原因，如果是模型有问题，则对模型进行完善和修改，如果是源代码出的问题，则修改相应功能实现代码，返回重新进行时间自动机模型的抽象。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人华东师范大学，其通讯地址为：200241 上海市闵行区东川路500号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。