Controller area network (CAN) is a high-speed serial fieldbus, widely deployed in the robot communication system. Due to the concurrency of service-oriented robot tasks and tightness requirement for real-time, it is necessary to explore how to refine the design model according to the bus protocol specifications and application system, in order to ensure the correctness and real-time requirements of the system and avoid bugs in design process. However the traditional methods are limited. This paper proposes a formal method to verify and analyze the correctness of CAN based fieldbus real-time control system. The model abstraction, formal modeling and automatic verification are presented for the system including the time automata model of master, joint controller, transceiver, arbitration and CAN bus. The formal models show that the worst arbitration delay of the low priority node increases rabidly with the increasing number of joints on the CAN bus. Furthermore, an improved dynamic priority strategy is designed and added into the formal models in order to improve the worst arbitration delay problem. The experimental results show that the deployment of the dynamic priority strategy not only reduces the arbitration delay of the low priority nodes, but also increases the capacity of nodes on CAN bus. The result provides guidance and effective reference for the system design.