Automatic verification of sequential control systems using temporal logic

Il Moon, Gary J. Powers, Jerry R. Burch, Edmund M. Clarke

Research output: Contribution to journalArticlepeer-review

28 Citations (Scopus)


Clarke et al. (1986) have developed a model‐based verification method and have applied it to validation of VLSI circuits. We have used the method to test automatically the safety and operability of discrete chemical process control systems. The technique involves: (1) a “system model” describing the process and its software; (2) “assertions” in temporal logic expressing user‐supplied questions about the system behavior with respect to safety and operability; and (3) a “model checker” that determines if the system model satisfies each of the assertions and provides a counterexample to locate the error if one exists. Temporal logic is used for reasoning about occurrence of events over time. To reveal discrete event errors, we have applied the verification method to a simple combustion system and an alarm acknowledge system.

Original languageEnglish
Pages (from-to)67-75
Number of pages9
JournalAIChE Journal
Issue number1
Publication statusPublished - 1992 Jan

All Science Journal Classification (ASJC) codes

  • Biotechnology
  • Environmental Engineering
  • Chemical Engineering(all)


Dive into the research topics of 'Automatic verification of sequential control systems using temporal logic'. Together they form a unique fingerprint.

Cite this