形式化方法在CAN总线机器人关节通信系统建模与验证中的应用

"这篇学术论文主要探讨了机器人关节通信总线系统的建模与验证方法，特别是在基于Controller Area Network (CAN) 的系统中的应用。作者们针对服务机器人的并发性和高实时性需求，提出使用形式化方法来建模和分析CAN现场总线型控制系统，旨在确保系统设计的正确性和实时性能。通过UPPAAL工具实现时间自动机模型，并进行了系统正确性验证和实时性分析。研究发现，随着CAN总线上关节节点数量增加，低优先级节点的仲裁时延增长加速。为解决此问题，文章提出了改进的动态优先级策略，并通过实验验证了该策略能有效减少低优先级节点的仲裁时延并提高总线的节点负载能力。" 本文是《软件学报》上发表的一篇研究论文，作者包括孟瑶、李晓娟、关永、王瑞和张杰。论文指出，在机器人通信系统中，CAN总线由于其高速串行特性而被广泛应用。服务机器人的任务特性对通信系统提出了高并发性和实时性的挑战。传统的设计方法可能无法充分满足这些需求，因此，研究者采用形式化方法来构建和验证基于CAN的控制系统模型。 在论文中，首先对系统进行了模型抽象和形式化表达，然后利用UPPAAL工具创建了包括主控制器、关节控制器、收发器、仲裁器和CAN总线在内的组件的时间自动机模型。通过这些模型，研究人员能够对机器人通信系统进行深入的正确性验证和实时性分析。 分析结果显示，关节节点数量的增加会导致低优先级节点的仲裁时延显著增长。为应对这一问题，研究者引入了一种改进的动态优先级策略，将其集成到形式模型中。实验表明，动态优先级策略成功地减少了低优先级节点的仲裁时延，并且增强了CAN总线的节点承载能力，为实际系统设计提供了理论依据和实践经验。 关键词涵盖了形式化验证、实时性、时间自动机、CAN总线以及动态优先级策略，表明本文的核心研究内容与这些技术密切相关。根据中国图书馆分类法，本文属于计算机科学和技术领域的 TP311 类别。