Title | Implicit model checking of logic-based control systems |

Publication Type | Journal Article |

Year of Publication | 1997 |

Authors | Park T, Barton PI |

Journal | AIChE Journal |

Volume | 43 |

Pagination | 2246-2260 |

Abstract | 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. |

URL | http://dx.doi.org/10.1002/aic.690430911 |

DOI | 10.1002/aic.690430911 |

# Implicit model checking of logic-based control systems

Submitted by tansh@mit.edu on