Software Engineering and Formal Methods

This work aims at demonstrating the benefits of integrating co-simulation and formal verification in the standard design flow of a brushless power drive system for precision robotic applications. A sufficient condition on controller gain for system stability is derived from the system’s mathematical model, including a control algorithm for the reduction of cogging torque. Then, using co-simulation and design space exploration, fine tuning of the controller gain parameters has been executed, exploiting the results from the formal verification.