Verification Of Programmable Logic Controllers
Tanneru Kameswara Rao,
M.Tech,
04,
32 pp.
Department of
Computer Science and Engineering
Indian Institute of Technology Bombay,
Powai, Mumbai 400 076.
Supervisor(s):
G.Sivakumar
Most of the control systems are hardwired, mean once they are built they cannot be modified. Programmable Logic Controllers (PLCs) were proposed as a standard for flexible implementation of Control Systems. Control Systems driven by PLCs are complex and safety critical. Small bugs in those systems can cause lot of damage to life. But PLCs are not tested exhaustively. PLC programs are being tested in a closed environment. In recent years various methods are being developed to verify PLC programs in a automated way. PLC programs are converted into equivalent verifiable SMV or Uppaal program. A set of specifications regarding PLC program were made. These specifications and verifiable code are fed to verifier for verification.
This report mainly concentrates on Ladder Diagrams and Sequential Fucntion Charts, languages for implementing PLCs. All the PLC programs discussed contain boolean variables only.