(625g) Verification of Control Systems with Discrete and Continuous Dynamics

The need for automated and safe control of chemical processes requires the analysis of dynamical systems with interdependencies between continuous controls and discrete switches. The continuous variables result from the application of classical controllers, such as PID and feedforward and more advanced controllers such as MPC. The discrete dynamics can be due to batch operation, mode switches during start-up and shut down of continuous processes, operator intervention or hardware or software failures. Systems that have integrated discrete and continuous dynamics are said to be hybrid.

The design of hybrid control systems remains an unsolved and potentially unsolvable problem (as shown by Prof. P. Varaiya). The design and testing of process automation systems therefore remains heuristic in nature and very much dependent on the knowledge, experience and the creativity of the personnel involved. Many tools, such as HAZOP, LOPA, Fault Trees etc exist. But these are are not exhaustive and the potential for errors persists. Increased process automation demands that ever more complex chemical process control systems with hybrid dynamics must be evaluated and faults in the control logic continue to occur and cause accidents.

The aim of this work is to examine the application of model checking to aid the testing of process automation systems that integrate discrete logic and continuous controls. For a given set of specifications, the system dynamics are modeled by representing the desired behavior as transitions between discrete states. These specifications are written as computation tree logic (CTL) formulas, and model checking is applied to the discrete abstraction of the continuous system. Current software systems such as nuSMV is capable of handling systems with well over 10E20 states in reasonable time. So very large logic systems can be checked. It is the abstraction (over-approximation) of the continuous dynamics rather than the discrete controls themselves that lead to combinatorial explosion. Making the abstract coarse makes the problem tractable However, if the abstraction is too coarse, or the specifications are too broad, then model checking mail fail to verify the specifications even though the system is actually correct.

To address the concern of inadequate specifications, this work relates the discrete states like alarms, trips and interlock to the continuous variables they rely on. This allows the verifier to build CTL formulas for the specifications based on the values of continuous variables in discrete time. A CTL specification may look like AG(SAFE)

where SAFE is a discrete variable that depends on a combination of continuous and discrete variables. The specification checks whether SAFE is false at any point in the execution of the discrete model, either due to faulty logic, too coarse of a discrete abstraction, or inadequate specifications. If false returns then the system provides a path that lead to failure. It may be a faulty measurement, as in the BP Texas City explosion, a low level alarm that is stuck or some other event that makes the system unobservable or uncontrallable.

The problem with coarse over approximations is solved by applying the SAFE condition to material and energy balances. Checking such balances lead to a tractable problem since mass and energy balances can be represented as integrators and can be solved with explicit integration. This approach theroefore presents a first step towards developing a comprehensive methodology for checking automation code in the chemical process industry.

A Liquid Holding Tank model formulation is included to demonstrate application of the model-checking solver NuSMV, highlighting that

(1) A model can be faulty and yet adhere to all logic and operational specifications at the same time.

(2) A fault in logic, combined with instrumentation failure, may lead to a critical state.

(3) Combination of instruments and safety logics can be suggested to ensure reliability of a unit even in the case of
multiple failures. The discrete state model is augmented with a continuous model in SIMULINK to verify the results of SMV.

The concept developed in this paper can be applied to test automation systems for chemical plants in a modular fashion. In some specific cases it will be possible to prove that the model satisfies the system specifications and that the specifications themselves are rich enough to account for all possible failures.