Formal Modeling and Verification of Motor Drive Software for Networked Motion Control Systems

Youngdong Kim (University of Seoul, Korea)

Ikhwan Kim (University of Seoul, Korea)

Inhye Kang (University of Seoul, Korea)

Taehyoun Kim (University of Seoul, Korea)

Minyoung Sung (University of Seoul, Korea)

Abstract: 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.

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

Categories: D.2.4, J.7