IMPLICIT MODEL CHECKING OF LOGIC-BASED CONTROL-SYSTEMS

Increasing automation in the CPI has led to the growing use of logic-b ased control systems (or safety interlock systems) in safety-related a nd sequencing operations. The growing complexity and safety-critical n ature of typical applications make developing technologies for the for mal verification of logic-based control systems with respect to their functionality a crucial and urgent issue It still remains elusive to a nalysis, primarily due to the exponential growth of the alternatives t hat must be examined with application size. Implicit model checking is a formal verification technology that can be applied to the verificat ion of large-scale logic-based control system. Its primary advantage i s to formally verify large-scale coupled systems, where a novel and co mpact model formulation makes tractable previously inaccessible proble ms. Logic-based control systems are represented compactly as an implic it Boolean state-space model, and the properties to be verified are re presented in the language of temporal logic. Verification is posed as a Boolean satisfiability problem and then transformed into its equival ent integer programming feasibility problem, which allows for efficien t solution with standard branch-and-bound algorithms. Benefits of the methodology are demonstrated by applying to large-scale industrial exa mples.