LAPSE:2023.25693
Published Article
LAPSE:2023.25693
Formal Verification and Co-Simulation in the Design of a Synchronous Motor Control Algorithm
March 29, 2023
Mechatronic systems are a class of cyber-physical systems, whose increasing complexity makes their validation and verification more and more difficult, while their requirements become more challenging. This paper introduces a development method based on model-based design, co-simulation and formal verification. The objective of this paper is to show the applicability of the method in an industrial setting. An application case study comes from the field of precision servo-motors, where formal verification has been used to find acceptable intervals of values for design parameters of the motor controller, which have been further explored using co-simulation to find optimal values. The reported results show that the method has been applied successfully to the case study, augmenting the current model-driven development processes by formal verification of stability, formal identification of acceptable parameter ranges, and automatic design-space exploration.
Keywords
co-simulation, cogging torque, formal verification, model-based design, power drive system, synchronous motor, theorem proving
Suggested Citation
Bernardeschi C, Dini P, Domenici A, Palmieri M, Saponara S. Formal Verification and Co-Simulation in the Design of a Synchronous Motor Control Algorithm. (2023). LAPSE:2023.25693
Author Affiliations
Bernardeschi C: Department of Information Engineering, University of Pisa, Via G. Caruso 16, 56127 Pisa, Italy [ORCID]
Dini P: Department of Information Engineering, University of Pisa, Via G. Caruso 16, 56127 Pisa, Italy [ORCID]
Domenici A: Department of Information Engineering, University of Pisa, Via G. Caruso 16, 56127 Pisa, Italy [ORCID]
Palmieri M: Department of Information Engineering, University of Pisa, Via G. Caruso 16, 56127 Pisa, Italy [ORCID]
Saponara S: Department of Information Engineering, University of Pisa, Via G. Caruso 16, 56127 Pisa, Italy [ORCID]
Journal Name
Energies
Volume
13
Issue
16
Article Number
E4057
Year
2020
Publication Date
2020-08-05
Published Version
ISSN
1996-1073
Version Comments
Original Submission
Other Meta
PII: en13164057, Publication Type: Journal Article
Record Map
Published Article

LAPSE:2023.25693
This Record
External Link

doi:10.3390/en13164057
Publisher Version
Download
Files
[Download 1v1.pdf] (1.1 MB)
Mar 29, 2023
Main Article
License
CC BY 4.0
Meta
Record Statistics
Record Views
65
Version History
[v1] (Original Submission)
Mar 29, 2023
 
Verified by curator on
Mar 29, 2023
This Version Number
v1
Citations
Most Recent
This Version
URL Here
https://psecommunity.org/LAPSE:2023.25693
 
Original Submitter
Auto Uploader for LAPSE
Links to Related Works
Directly Related to This Work
Publisher Version