Verificação e síntese de controladores de realimentação de estados estática com garantias formais de desempenho não frágil

Abstract

In this work, we describe an approach to perform verification and synthesis in discrete control systems with state feedback over step response performance requirements in control systems which is based on counterexample-guided inductive synthesis techniques (CEGIS). In this approach there is a performance requirement (e.g., settling time and maximum overshoot) in a given control system in order to know if it satisfies the desired value for that requirement, if it does not satisfy, one must find a system that satisfies the desired requirement, in which case the system controller is reset. For the generation of the controller, we use a learning technique where each iteration that the verification of the requirement does not satisfy, we learn that this controller is not worthy. In the verification of these performance requirements in discrete control systems, we consider the fragility (numerical quantization error, round-offs, etc.) in the controllers used. This approach is useful for assisting control engineers in their discrete control systems projects since such weaknesses occur during implementation on a digital platform, in which case this approach generates the system that meets the requirements desired in the design. This approach was implemented using DSVerifier which is a tool that employs bounded (and unbounded) model verification based on satisfiability modulo theories. Our approach was evaluated in a set of classical control system benchmarks extracted from the control literature, as well as in specific benchmarks considering different eigenvalues. The experimental results show that the elaborated approach is effective for the synthesis of performance requirements in discrete state feedback control systems since it considers practical implementation problems (FWL effects), unlike other methods that routinely do not consider these problems.