Automatic verification of sequential control systems using temporal logic

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

Research output: Contribution to journalArticle

65 Citations (Scopus)

Abstract

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
Volume38
Issue number1
DOIs
Publication statusPublished - 1992 Jan

Fingerprint

Temporal logic
Control systems
Chemical Phenomena
Safety
VLSI circuits
Alarm systems
Process control
Software

All Science Journal Classification (ASJC) codes

  • Biotechnology
  • Environmental Engineering
  • Chemical Engineering(all)

Cite this

Moon, Il ; Powers, Gary J. ; Burch, Jerry R. ; Clarke, Edmund M. / Automatic verification of sequential control systems using temporal logic. In: AIChE Journal. 1992 ; Vol. 38, No. 1. pp. 67-75.
@article{57d462226a8d47f1a399a620e5f24893,
title = "Automatic verification of sequential control systems using temporal logic",
abstract = "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.",
author = "Il Moon and Powers, {Gary J.} and Burch, {Jerry R.} and Clarke, {Edmund M.}",
year = "1992",
month = "1",
doi = "10.1002/aic.690380107",
language = "English",
volume = "38",
pages = "67--75",
journal = "AICHE Journal",
issn = "0001-1541",
publisher = "American Institute of Chemical Engineers",
number = "1",

}

Automatic verification of sequential control systems using temporal logic. / Moon, Il; Powers, Gary J.; Burch, Jerry R.; Clarke, Edmund M.

In: AIChE Journal, Vol. 38, No. 1, 01.1992, p. 67-75.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Automatic verification of sequential control systems using temporal logic

AU - Moon, Il

AU - Powers, Gary J.

AU - Burch, Jerry R.

AU - Clarke, Edmund M.

PY - 1992/1

Y1 - 1992/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=0026617165&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0026617165&partnerID=8YFLogxK

U2 - 10.1002/aic.690380107

DO - 10.1002/aic.690380107

M3 - Article

AN - SCOPUS:0026617165

VL - 38

SP - 67

EP - 75

JO - AICHE Journal

JF - AICHE Journal

SN - 0001-1541

IS - 1

ER -