TY - JOUR
T1 - Formal modeling and verification of motor drive software for networked motion control systems
AU - Kim, Youngdong
AU - Kim, Ikhwan
AU - Kang, Inhye
AU - Kim, Taehyoun
AU - Sung, Minyoung
N1 - Publisher Copyright:
© J.UCS.
PY - 2014
Y1 - 2014
N2 - This paper presents a model-based approach to the design and verification of motor drive software for networked motion control systems. We develop a formal model for an Ethernet-based motion system, where, using timed automata, we describe the concurrent and synchronized behaviors 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 accuracy of 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 demonstrate the 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-time schedulability 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 and accuracy.
AB - This paper presents a model-based approach to the design and verification of motor drive software for networked motion control systems. We develop a formal model for an Ethernet-based motion system, where, using timed automata, we describe the concurrent and synchronized behaviors 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 accuracy of 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 demonstrate the 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-time schedulability 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 and accuracy.
KW - Actuation delay and deviation
KW - Formal methods
KW - Formal methods
KW - Motor drive software
KW - Timed automata
UR - http://www.scopus.com/inward/record.url?scp=84923028024&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:84923028024
SN - 0948-695X
VL - 20
SP - 1903
EP - 1925
JO - Journal of Universal Computer Science
JF - Journal of Universal Computer Science
IS - 14
ER -