Predictive Control And Formal Verification Technology Using MLD Model

In the modern process industry, process control objects are day by day complex and the precision control becomes higher and higher, the coupled relation between the continuous variables dynamic systems and the discrete event dynamic systems which are in the process of industrial control is increasing obviously. The traditional theoretical methods to the modeling and control of these systems have been difficult to achieve control requirements. To consider these conditions, this paper makes use of mixed logical dynamical (MLD) model to study the modeling, control and formal verification of hybrid system.Based on the previous research, the paper makes a further research and exploration of the theory of hybrid system. Research contents include control and formal verification of hybrid system based on MLD model, main research works and achievements are summarized as following:This paper deeply studies the mechanism of MLD system, the method of logical propositional calculus and linear integer programming. The MLD model of CSTR system is described by the mechanism modeling and the Hysdel method respectively.And summarizes the equivalence between different models of hybrid system.The traditional model predictive control (MPC) is applied to the MLD system. we studies the open-loop constrained optimal control of the MLD system, separately discusses MPC scheme based on MIQP and the MILP problem. The simulation results authenticate the effectiveness of the two methods.Formal verification methods of hybrid system, theorem proving and model checking, are discussed in detail, and formal verification tools based on model checking are introduced. The formal verification simulation research has been conducted to the bouncing ball system using the CheckMate tool.Propose formal verification questions of hybrid MLD system, in view of the mixed logical dynamic system, deeply research a approach to the verification of hybrid systems based on linear and mixed-integer linear programming. The approach is demonstrated on a verification case study for CSTR system. Discuss the safety problem of CSTR system, and make a beneficial exploration to the hybrid system control's accuracy and reliability.At the end of this paper,the research work is summarized,and the prospect about the development trend of hybrid system control and formal verification technology are carried out.