Verification and optimization of a PLC control schedule

Ed Brinksma, Angelika Mader, Ansgar Fehnker

Research output: Contribution to journalArticlepeer-review

24 Citations (Scopus)


We report on the use of model checking techniques for both the verification of a process control program and the derivation of optimal control schedules. Most of this work has been carried out as part of a case study for the EU VHS project (Verification of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to be designed and verified. The original intention of our approach was to see how much could be achieved here using the standard model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite expensive it is interesting to try and exploit the efficiency of established non-real-time model checkers like SPIN in those cases where promising work-arounds seem to exist. In our case we handled the relevant real-time properties of the PLC controller using a time-abstraction technique; for the scheduling we implemented in Promela a so-called variable time advance procedure. To compare and interpret the results we carried out the same case study with the aid of the real-time model checker Uppaal, enhanced with facilities for cost-guided state space exploration. Both approaches proved sufficiently powerful to verify the design of the controller and/or derive (time-)optimal schedules within reasonable time and space requirements.
Original languageEnglish
Pages (from-to)21-33
Number of pages13
JournalInternational Journal on Software Tools for Technology Transfer
Issue number1
Publication statusPublished - Oct 2002
Externally publishedYes


  • Formal methods
  • Verification
  • Model checking
  • Hybrid systems
  • Scheduling


Dive into the research topics of 'Verification and optimization of a PLC control schedule'. Together they form a unique fingerprint.

Cite this