Sound, Automated, and scalable, Synthesis of Digital Controllers for Physical Systems

点击翻译按钮获取中文摘要

Brief description of the context of the research including potential impact: Connections between verification and control underpin work on the development of symbolic methods and automated techniques based on SAT/SMT theory for the synthesis of CPS.This project will employ powerful techniques from bounded model checking and inductive synthesis (CEGIS and SyGuS) to automatically design sound digital controllers for physical plants (1,2). The approach allows for the design and synthesis of modern control architectures, implemented over digital devices such as FPGAs using automatic procedures that are correct by construction. The synthesis is sound with respect to the complete range of approximates related to utilising digital architectures for physical plants including: time discretisation, quantisation and saturation effects, and finite-precision arithmetics with rounding errors.Aims and Objectives: The end-goal of this project is to contribute towards the development of a new, automated, sound and scalable framework, improving industrially relevant state-of-the-art results in digital control systems. Novelty of the Research Method: Recently (3) has employed the CEGIS architecture to automatically and soundly synthesise Lyapunov control functions for control systems, successfully using neural networks as templates for Lyapunov functions. This project seeks to extend this work to synthesisng controllers of physical systems. Alignment to EPSRC's strategies and research areas: This project will be in line with EPSRC's research areas in Verification and correctness and control engineering.(1) A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening and E. Polgreen, Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants, CAV17, LNCS 10426, pp 462-482, 2017.(2) A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening and E. Polgreen, Automated Formal Synthesis of Provably Safe Digital Controllers for Continuous Plants, Acta Informatica, In Press, 2020.(3) D. Ahmed, A. Peruffo and A. Abate, Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers, TACAS20, To Appear, 2020.