Abstract

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 languageUndefined
Pages (from-to)21-33
Number of pages13
JournalInternational journal on software tools for technology transfer
Volume4
Issue number1
DOIs
StatePublished - 2002

Fingerprint

Model checking
Programmable logic controllers
Controllers
Chemical plants
Hybrid systems
Process control
Scheduling
Costs

Keywords

  • EWI-873
  • METIS-209590
  • IR-38269

Cite this

@article{d3a17d4526524bdf98daa8dc12a1c32a,
title = "Verification and Optimization of a PLC Control Schedule",
abstract = "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.",
keywords = "EWI-873, METIS-209590, IR-38269",
author = "Hendrik Brinksma and Mader, {Angelika H.} and Ansgar Fehnker and Ansgar Fehnker",
note = "Imported from DIES",
year = "2002",
doi = "10.1007/s10009-002-0079-0",
volume = "4",
pages = "21--33",
journal = "International journal on software tools for technology transfer",
issn = "1433-2779",
publisher = "Springer Berlin Heidelberg",
number = "1",

}

TY - JOUR

T1 - Verification and Optimization of a PLC Control Schedule

AU - Brinksma,Hendrik

AU - Mader,Angelika H.

AU - Fehnker,Ansgar

AU - Fehnker,Ansgar

N1 - Imported from DIES

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

KW - EWI-873

KW - METIS-209590

KW - IR-38269

U2 - 10.1007/s10009-002-0079-0

DO - 10.1007/s10009-002-0079-0

M3 - Article

VL - 4

SP - 21

EP - 33

JO - International journal on software tools for technology transfer

T2 - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

SN - 1433-2779

IS - 1

ER -