Formal modeling and verification of motor drive software for networked motion control systems

Youngdong Kim, Ikhwan Kim, Inhye Kang, Taehyoun Kim, Minyoung Sung

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

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

Original languageEnglish
Pages (from-to)1903-1925
Number of pages23
JournalJournal of Universal Computer Science
Volume20
Issue number14
StatePublished - 2014

Keywords

  • Actuation delay and deviation
  • Formal methods
  • Formal methods
  • Motor drive software
  • Timed automata

Fingerprint

Dive into the research topics of 'Formal modeling and verification of motor drive software for networked motion control systems'. Together they form a unique fingerprint.

Cite this