Premium
Automatic verification of sequential control systems using temporal logic
Author(s) -
Moon Il,
Powers Gary J.,
Burch Jerry R.,
Clarke Edmund M.
Publication year - 1992
Publication title -
aiche journal
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.958
H-Index - 167
eISSN - 1547-5905
pISSN - 0001-1541
DOI - 10.1002/aic.690380107
Subject(s) - operability , computer science , temporal logic , model checking , counterexample , event (particle physics) , process (computing) , programming language , simple (philosophy) , algorithm , real time computing , mathematics , software engineering , philosophy , physics , epistemology , discrete mathematics , quantum mechanics
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.