模型 based on the bus protocol specification and application demands, ensuring system correctness and real-time performance to avoid flaws during the design phase. In response to the limitations of traditional methods, this paper proposes a formal method for modeling and analysis of control systems based on CAN (Controller Area Network) fieldbuses.
The authors, Meng Yao, Li Xiaojuan, Guan Yong, Wang Rui, and Zhang Jie, from the College of Information Engineering at Capital Normal University, the Beijing Key Laboratory of Light Industrial Robot and Safety Verification, and the College of Information Science & Technology at Beijing University of Chemical Technology, have conducted research focusing on the modeling and verification of robot joint communication bus systems. They emphasize the importance of CAN in robot communication systems due to its high-speed serial nature, which is crucial for meeting the concurrent and real-time requirements of service robots.
In their work, they first abstract and formally express the system model. Using the UPPAAL tool, they construct time automata models for the main controller, joint controllers, transceivers, arbiter, and the CAN bus. This formal modeling and automatic verification process enables the researchers to validate the correctness of the robot communication system and analyze its real-time properties.
The analysis reveals that as the number of joint nodes on the bus increases, the worst-case arbitration latency for low-priority nodes grows significantly. To address this issue, the authors introduce an improved dynamic priority strategy into the formal model. The experimental results demonstrate that implementing this dynamic priority strategy reduces arbitration latency for low-priority nodes and also increases the node load capacity of the CAN bus, providing valuable guidance and reference for system design.
The key aspects of this study include formal verification, real-time performance, time automata, and dynamic prioritization in the context of CAN-based communication systems. By utilizing formal methods, the authors contribute to enhancing the reliability and efficiency of robotic systems, particularly in terms of communication and concurrency management.
This work is significant because it highlights the need for rigorous modeling and validation techniques in the development of complex robotic systems, especially those relying on communication buses like CAN. The proposed approach not only contributes to improving the overall performance of robots but also paves the way for future advancements in the field of robotics and automation, where communication efficiency and real-time responsiveness are of utmost importance.
In conclusion, the research presented in "Robot Joint Bus Communication System's Modeling and Verification" provides valuable insights into the challenges and solutions for optimizing the design and operation of communication systems in robots. The integration of formal methods, combined with dynamic priority strategies, offers a promising approach to mitigate issues related to concurrency and real-time constraints in the rapidly evolving world of robotics.
