Control And Formal Verification Of Hybrid System Using MLD Model

With the increasing complexity of process control objects, hybrid feature exists widely in process industries. According this situation, this dissertation studies the control and formal verification issues of hybrid systems using Mixed Logical Dynamical (MLD) model. A hybrid predictive control algorithm is studied and then applied to a process with serious nonlinearity; the dissertation also presented a formal verification algorithm, basing on MLD model. This dissertation focus on applying the hybrid control algorithm and hybrid formal verification algorithm on a CSTR (Continuous Stirred Tank Reactor) process. The CSTR process is controlled using hybrid predictive control algorithm to investigate how to drive the process to the steady state smoothly and quickly. Thus a new control strategy for CSTR process has been presented. Formal verification technique is used to verify safety issues in CSTR process for the first time. This research provides warranty to operate the CSTR under safety states.Main research works and achievements are summarized as following:MLD modeling technique and approach are studied. By comparing the difference between general proposional logic modeling method and HYSDEL software method, the thesis gives a rule to select modeling method according to different systems. The model of CSTR process was developed and simulated using these two methods.Basing on MLD model, hybrid optimal control algorithm and hybrid predictive control algorithm are studied. The optimal control algorithms are applied to the CSTR process with infinite norm and 2-norm performance index. Simulation results show that the hybrid optimal control algorithm can drive the CSTR process to the steady state smoothly and quickly. Oscillation phenomenon is avoided while the process states switching between piecewise models.Different formal verification algorithms for hybrid system are introduced and compared. A concentration control system and a bouncing ball system are used to illustrate the hybrid formal verification algorithm and procedure by using CheckMate tool. Advantages and disadvantages of using CheckMate tool are summarized.At last, Formal verification algorithm based on MLD model is studied for the first time. The algorithm implements by solving the reach set computation. Basing on the MLD model of CSTR process, the algorithm is simulated and illustrated. Thus formal verification technique for the CSTR process is developed. Warranty to operate the CSTR under safety states can be obtained.Detail simulations for the theory and algorithm discussed in the dissertation are given by controlling the CSTR process. Simulation results show promising performance in the hybrid optimal control and hybrid formal verification for the CSTR process. The dissertation presents a new control strategy for serious nonlinear CSTR process.