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 largescale industrial examples.