This paper presents a model-based approach to the design and verification of motordrive software for networked motion control systems. We develop a formal model for an Ethernetbased motion system, where, using timed automata, we describe the concurrent and synchronizedbehaviors of the components, i.e., motion controller, motor drives, and communication links. The drive, in particular, is modeled in enough detail to accurately reflect the software implementa-tion used in a real drive. We use the design of multitasked drive software with fixed-priority preemptive scheduling. With UPPAAL model checking, we verify the precision and accuracyof the rendered motion in terms of the requirements on the actuation delay at each drive and the actuation deviation between different drives, respectively. The analysis results demonstratethe benefits of our model-based approach in the safety verification and design space exploration of motor drive software. We show that it is possible to verify deadlock freeness and real-timeschedulability in an early design phase. And, for varying number of drives and size of messages, we can successfully determine the combination of task periods that leads to the best precision andaccuracy.

timed automata, formal methods, motor drive software, formal methods, Actua-tion delay and deviation