Verification and synthesis of linear systems by abstract acceleration

Embedded systems are constantly growing in number and complexity. A large number of these relate to physical elements that have behaviour that is either linear or can be described using linear dierential equations (e.g., vehicle speed/position, temperature control, oscillators, etc). In this work we explore the application of formal methods for safety checking and controller synthesis in the particular case of Linear Time Invariant (LTI) models where the dynamics may apply to both continuous and discrete variables in both continuous and discrete time. Our work applies to each of these cases independently. To this end, we use abstract acceleration, a method that combines abstract interpretation with acceleration in order to compute precise fix-points for the reach space of the model. Existing techniques have proven to be useful in the verification of discrete time systems, and we extend the method to a wider set of models and improve its performance. Furthermore, by applying control theory and SAT solving techniques, we explore the synthesis of correct by construction digital controllers using abstract acceleration as a model template. Our results show that the technique scales to models with several dozen variables for which sound results can be found in a matter of minutes.