Correct-by-construction control synthesis for buck converters with event-triggered state measurement

In this paper, we illustrate a new correct-by-construction switching controller for a power converter with event-triggered measurements. The event-triggered measurement scheme is beneficial for high frequency power converters because it requires relatively low-speed sampling hardware and is immune to unmodeled switching transients. While providing guarantees on the closed-loop system behavior is crucial in this application, off-the-shelf abstraction-based techniques cannot be directly employed to synthesize a controller in this setting because controller cannot always get instantaneous access to the current state. As a result, the switching action has to be based on slightly out-of-date measurements. To tackle this challenge, we introduce the out-of-date measurement as an extra state variable and project out the inaccessible real state to construct a belief space abstraction. The properties preserved by this belief space abstraction are analyzed. Finally, an abstraction-based synthesis method is applied to this abstraction. We demonstrate the controller on a constant on-time buck voltage regulator plant with an event-triggered sampler. The simulation verifies the effectiveness of our controller.