(703b) Error Detection for Chemical Plant Automation Logic Using Model Checking and Supervisory Control Theory

Analyzing the automation logic in a modern chemical plant requires
systematic tools, due to the complexity of the discrete logic itself,
as well as its interaction with the continuous process dynamics.  The
interaction between the discrete dynamics of the automation system and
the continuous dynamics of the chemical process results in a hybrid
system.  Such systems are notoriously difficult to analyze due to the
rapid explosion of the number of discrete states and the need to
integrate differential equations to track the evolution of the
continuous variables between discrete transitions.  The number of
discrete states in a typical industrial system may be $10^{100}$ or
more.

The purpose of this work is to examine the application of a
recently-developed method for detecting errors in the discrete logic
of hybrid systems.  We propose to apply supervisory control theory to
reduce the error-detection problem for hybrid systems to a tractable
discrete problem.  The class of errors that this approach can detect
includes the reachability of forbidden/undesirable discrete states, or
situations in which a particular piece of equipment is prevented from
ever switching on.

In the current paper we formulate the error detection problem as a
series of computation tree logic (CTL) specifications of the form
$AG(p_1 \wedge EF(p_2))$, which must be satisfied for the system
to be free of errors.  This type of specification mirrors the classic
controllability and non-blocking requirement of supervisory control
theory, which was developed by Ramadge and Wonham for discrete event
systems.  Symbolic model checking (which has previously been applied
to verify discrete logic in chemical plant automation systems) is used
at the core of our error-detection algorithm, along with the
aforementioned supervisory control theory, to check if the
specification can be satisfied.  The combination of these techniques
is novel in that it expands the class of logical errors which can be
detected in hybrid systems without explicitly evaluating the
continuous dynamics.

The method we develop in this research relies on conservative
approximation of the system dynamics to ensure that an error is
reported only if it is guaranteed to violate one of the
specifications.  We provide both process-independent tests, which
should apply to any control system, and process-dependent tests that
address specific aspects of a particular plant's operation.  All of
the specifications presented in this work are of the form mentioned
previously, and therefore are compatible with the methods we develop.
A sample problem, motivated by an industrial collaboration with The
Dow Chemical Company, is included to demonstrate the application of
the presented methods.