Note: This content is accessible to all versions of every browser. However, this browser does not seem to support current Web standards, preventing the display of our site's design details.


Safety guarantees via formal verification


M. Morari

AIChE Annual Meeting, Los Angeles, USA

Typically in control theory we are interested in controlling a process to follow a specified trajectory with minimum error. In practice, it is more important to guarantee with the control system that the process can never enter an undesirable ("unsafe") operating region. For example, emergency override and shut down procedures have to be designed properly to prevent such excursions under all foreseeable operating conditions, disturbances, process parameters etc. For a formal guarantee of safety two problems need to be addressed. First we need to devise a model form which is expressive enough to describe the dynamic system together with its control system which includes logic and switches. Second we need to develop an efficient procedure to verify that with the designed control system the unsafe operating region is always avoided. The paper reports a new efficient verification procedure based on the Mixed Logical Dynamical (MLD) modelling formalism introduced previously by the authors. We demonstrate the effectiveness of the procedure on the batch evaporator benchmark example (Kowalewski, 1998). It involves three continuous states and a finite state automaton representing a PLC control sequence. The problem is described in the HYSDEL language and the MLD model is generated automatically by our compiler.


Type of Publication:


No Files for download available.
% No recipe for automatically generating a BibTex entry for (06)Talk
Permanent link