Modeling Programmable Logic Controllers for Logic Verification

Research output: Contribution to journalArticlepeer-review

90 Citations (Scopus)


Verification method has been developed for determining the safety and operability of programmable logic controller (PLC) based systems. The method automatically checks sequential logic embedded in PLCs and provides counterexamples if it finds errors. The method consists of a system model, assertions, and a model checker. The model is a Boolean-based representation of a PLC's behavior. Assertions are questions about the behavior of the system, expressed in temporal logic. The model checker generates a state space based on the above two inputs, searches the space efficiently, determines the consistency of the model and assertions, and supplies counterexamples. A modeling technique has been developed to verify relay ladder logic (RLL), a PLC programming language. The performance of the model checker is studied in a series of alarm designs.

Original languageEnglish
Pages (from-to)53-59
Number of pages7
JournalIEEE Control Systems
Issue number2
Publication statusPublished - 1994 Apr

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • Modelling and Simulation
  • Electrical and Electronic Engineering


Dive into the research topics of 'Modeling Programmable Logic Controllers for Logic Verification'. Together they form a unique fingerprint.

Cite this