Hybrid formal verification of CSTR system based on MLD model

The operation safety problems in process industry are becoming more and more important. Based on Mixed Logical Dynamical (MLD) model, operation safety problems are converted into hybrid formal verification problems in this paper. The hybrid formal verification algorithm is applied to a CSTR process with serious nonlinearity. By defining safety states as reach set, the CSTR process is modeled in the MLD form. Then operation safety problems of CSTR can be transformed into hybrid formal verification problems. The safety reach sets are computed by MPT software. Simulation results show that CSTR process can be driven to safety reach sets with proper control action calculated using hybrid formal verification algorithm. This paper illustrates the effectiveness of this hybrid formal verification method and provides a novel approach to handle operation safety problems in process industry.