Paper Info
Title
Formal Modeling and Verification of Motor Drive Software for Networked Motion Control Systems.
Abstract
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 implementation 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.
Year
Venue
Keywords
2014
JOURNAL OF UNIVERSAL COMPUTER SCIENCE
Timed automata,Formal methods,Motor drive software,Formal methods,Actuation delay and deviation
Field
DocType
Volume
Data mining,Combinatorics,Computer science
Journal
20
Issue
ISSN
Citations 
14
0948-695X
0
PageRank 
References 
Authors
0.34
19
5
Name
Order
Citations
PageRank
Youngdong Kim100.34
Ikhwan Kim271.29
Inhye Kang316917.91
Taehyoun Kim400.34
M. Sung500.68