-A A +A

Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants

TitleSafe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
Publication TypeConference Paper
Year of Publication2018
AuthorsAbate A, Bessa I, Cattaruzza D, Cordeiro L, David C, Kessell P, Kroening D, Polgreen E
Conference Name7th Workshop on Synthesis
Date Published07/2018

We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as linear, time-invariant models. The synthesis accounts for errors caused by the digitization effects introduced by digital controllers operating in either fixed-or floating-point arithmetic. Our approach uses counterexample-guided inductive synthesis (CEGIS): in the first phase an inductive generalisation engine produces a possible solution that is safe for some possible initial conditions but may not be safe for all initial conditions. Safety for all initial conditions is then verified in a second phase either via bounded model checking or abstract acceleration; if the verification step fails, a counterexample is provided to the inductive generalisation and the process iterates until a safe controller is obtained. We implemented our approach in a tool named DSSynth (Digital-System Synthesizer) and demonstrate its practical value by automatically synthesizing safe controllers for physical plant models from the digital control literature. 


Oxford Control and Verification (OXCAV) Group

C/O Department of Computer Science

Wolfson Building, Parks Rd, Oxford OX1 3QD

T: +44 (0) 18656 10767

Education - This is a contributing Drupal Theme
Design by WeebPal.