ISSN:
0001-1541
Keywords:
Chemistry
;
Chemical Engineering
Source:
Wiley InterScience Backfile Collection 1832-2000
Topics:
Chemistry and Pharmacology
,
Process Engineering, Biotechnology, Nutrition Technology
Notes:
Increasing automation in the CPI has led to the growing use of logic-based control systems (or safety interlock systems) in safety-related and sequencing operations. The growing complexity and safety-critical nature of typical applications make developing technologies for the formal verification of logic-based control systems with respect to their functionality a crucial and urgent issue. It still remains elusive to analysis, primarily due to the exponential growth of the alternatives that must be examined with application size. Implicit model checking is a formal verification technology that can be applied to the verification of large-scale logic-based control system. Its primary advantage is to formally verify large-scale coupled systems, where a novel and compact model formulation makes tractable previously inaccessible problems. Logic-based control systems are represented compactly as an implicit Boolean state-space model, and the properties to be verified are represented in the language of temporal logic. Verification is posed as a Boolean satisfiability problem and then transformed into its equivalent integer programming feasibility problem, which allows for efficient solution with standard branch-and-bound algorithms. Benefits of the methodology are demonstrated by applying to largescale industrial examples.
Additional Material:
22 Ill.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1002/aic.690430911
Permalink
