Implicit model checking of logic-based control systems

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 large-scale industrial examples.