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.
|Number of pages||2|
|Publication status||Published - 18 May 2018|
|Event||Seventh Workshop on Synthesis - Oxford, United Kingdom|
Duration: 18 Jul 2018 → 18 Jul 2018
|Workshop||Seventh Workshop on Synthesis|
|Abbreviated title||SYNT 2018|
|Period||18/07/18 → 18/07/18|