Explicit Model Predictive Control And Formal Verification Based On PWA Model

Piecewise affine(PWA)model can not only describe the nonlinear and hybird characteristics of a system,but also is convenient for performance analysis and research of control methods of a system.So it has received extensive attention in control field.In this thesis,an explicit model predictive control method based on PWA model is researched,and then several algorithms are used to improve the real-time control performance.In order to verify operation safety and reliability of a system,a formal verification method based on PWA model is proposed.This method is capable of predicting whether the system exists hidden danger.All the research achievements have been applied to a continuous stirred tank reactor(CSTR)system and two tank system to show their effectiveness.The main research works are summarized as follows:A method of modeling a PWA model is studied.A CSTR system with a typical nonlinear characteristic and a two tank system with a typical hybrid feature are modeled in PWA form respectively.An explicit model predictive control method based on PWA model is researched.In this method,an explicit control law is obtained by solving an optimization problem offline using a dynamic programming strategy together with a multi-parametric solver,thus online computation cost is greatly reduced.And several modified algorithms are used to speed up the online computation by simplifying partitions of the explicit controller or improving the point location algorithm.Based on the above method,an active fault tolerant control algorithm is investigated.In the proposed algorithm,a piecewise affine fault model is established and an explicit fault tolerant controller is obtained,so that a system can achieve acceptable performance and stability properties in either the normal or fault situations.A formal verification method based on PWA model is proposed for verifying the security and reliability of a system.The method can verify safety properties of a system with bounded inputs and additive disturbances or under an explicit controller via forward or backward reachability analysis.An active fault diagnosis method is then proposed using the verification method mentioned above.It can detect the fault information of a system by observing the system behaviours when a corresponding test signal excites the system.