Formal verification of PLC programs

  • Rausch M
  • Krogh B
  • 36


    Mendeley users who have this article in their library.
  • 41


    Citations of this article.


This paper presents an approach to the verification of programs
for programmable logic controllers (PLCs) using SMV, a software package
for formal verification of state transition systems. Binary PLC programs
are converted directly into SMV modules that retain the variable names
and execution sequences of the original programs. The system being
controlled is modeled by a C/E system block diagram which is also
transformed into a set of SMV modules, retaining the structure of the
block diagram model. SMV allows the engineer to verify the behavior of
the control program over all possible operating conditions. Mechanisms
are discussed for representing correctly the concurrent execution of the
PLC programs and the plant model using SMV primitives. The SMV approach
to PLC program verification is illustrated with an example

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • M. Rausch

  • B. H. Krogh

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free