From differential equations to finite state machines: A new approach for formal verification of chemical processes models

In chemical process design or operation, mathematical model simulation can be used to ensure safety or stability. The application of formal verification, nowadays employed in the hardware and software industry to verify properties, is an alternative method. However, most process simulation models differ from formal verification models. The problem is how to reconcile these models to be used in a single project. This article proposes a methodology to integrate computational models usually used for simulation in the chemical engineering industry with the state-based models used for formal verification. At first, the dynamic behavior of processes, obtained from various simulation models, generates intermediate descriptions that are converted into suitable state-based models (finite-state machines). The new models are further used to verify the required properties. The proposed methodology is applied to a chemical reactor model based on differential equations. Temporal Logic (employing NuSMV) is used to verify properties such as the existence of multiple steady states and generate startup procedures to reach a desired steady state. The model’s transformation phase is validated by contrasting the original model with the created model, demonstrating that simulation models align with formal verification models. The transformation contributes to the of use formal verification to complement simulation in process engineering design.