Verification and Optimization of a PLC Control Schedule

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

20 Citations (Scopus)
44 Downloads (Pure)

Abstract

We report on the use of the SPIN model checker for both the verification of a process control program and the derivation of optimal control schedules. This work was carried out as part of a case study for the EC 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 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. For this case study these techniques proved sufficient to verify the design of the controller and derive (time-)optimal schedules with reasonable time and space requirements.
Original languageUndefined
Title of host publication7th Int. SPIN Workshop on Model Checking of Software
EditorsK. Havelund, J. Penix, W. Visser
Place of PublicationBerlin
PublisherSpringer
Pages73-92
Number of pages20
ISBN (Print)3-540-41030-9
DOIs
Publication statusPublished - Aug 2000
Event7th International SPIN Workshop on SPIN Model Checking and Software Verification 2000 - Stanford, United States
Duration: 30 Aug 20001 Sep 2000
Conference number: 7

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1885

Workshop

Workshop7th International SPIN Workshop on SPIN Model Checking and Software Verification 2000
CountryUnited States
CityStanford
Period30/08/001/09/00

Keywords

  • EWI-984
  • METIS-119632
  • IR-19109

Cite this

Brinksma, H., & Mader, A. H. (2000). Verification and Optimization of a PLC Control Schedule. In K. Havelund, J. Penix, & W. Visser (Eds.), 7th Int. SPIN Workshop on Model Checking of Software (pp. 73-92). (Lecture Notes in Computer Science; Vol. 1885). Berlin: Springer. https://doi.org/10.1007/10722468_5
Brinksma, Hendrik ; Mader, Angelika H. / Verification and Optimization of a PLC Control Schedule. 7th Int. SPIN Workshop on Model Checking of Software. editor / K. Havelund ; J. Penix ; W. Visser. Berlin : Springer, 2000. pp. 73-92 (Lecture Notes in Computer Science).
@inproceedings{2269efa7366f4f198a4884a6782f781b,
title = "Verification and Optimization of a PLC Control Schedule",
abstract = "We report on the use of the SPIN model checker for both the verification of a process control program and the derivation of optimal control schedules. This work was carried out as part of a case study for the EC 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 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. For this case study these techniques proved sufficient to verify the design of the controller and derive (time-)optimal schedules with reasonable time and space requirements.",
keywords = "EWI-984, METIS-119632, IR-19109",
author = "Hendrik Brinksma and Mader, {Angelika H.}",
note = "Imported from DIES",
year = "2000",
month = "8",
doi = "10.1007/10722468_5",
language = "Undefined",
isbn = "3-540-41030-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "73--92",
editor = "K. Havelund and J. Penix and W. Visser",
booktitle = "7th Int. SPIN Workshop on Model Checking of Software",

}

Brinksma, H & Mader, AH 2000, Verification and Optimization of a PLC Control Schedule. in K Havelund, J Penix & W Visser (eds), 7th Int. SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science, vol. 1885, Springer, Berlin, pp. 73-92, 7th International SPIN Workshop on SPIN Model Checking and Software Verification 2000, Stanford, United States, 30/08/00. https://doi.org/10.1007/10722468_5

Verification and Optimization of a PLC Control Schedule. / Brinksma, Hendrik; Mader, Angelika H.

7th Int. SPIN Workshop on Model Checking of Software. ed. / K. Havelund; J. Penix; W. Visser. Berlin : Springer, 2000. p. 73-92 (Lecture Notes in Computer Science; Vol. 1885).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Verification and Optimization of a PLC Control Schedule

AU - Brinksma, Hendrik

AU - Mader, Angelika H.

N1 - Imported from DIES

PY - 2000/8

Y1 - 2000/8

N2 - We report on the use of the SPIN model checker for both the verification of a process control program and the derivation of optimal control schedules. This work was carried out as part of a case study for the EC 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 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. For this case study these techniques proved sufficient to verify the design of the controller and derive (time-)optimal schedules with reasonable time and space requirements.

AB - We report on the use of the SPIN model checker for both the verification of a process control program and the derivation of optimal control schedules. This work was carried out as part of a case study for the EC 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 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. For this case study these techniques proved sufficient to verify the design of the controller and derive (time-)optimal schedules with reasonable time and space requirements.

KW - EWI-984

KW - METIS-119632

KW - IR-19109

U2 - 10.1007/10722468_5

DO - 10.1007/10722468_5

M3 - Conference contribution

SN - 3-540-41030-9

T3 - Lecture Notes in Computer Science

SP - 73

EP - 92

BT - 7th Int. SPIN Workshop on Model Checking of Software

A2 - Havelund, K.

A2 - Penix, J.

A2 - Visser, W.

PB - Springer

CY - Berlin

ER -

Brinksma H, Mader AH. Verification and Optimization of a PLC Control Schedule. In Havelund K, Penix J, Visser W, editors, 7th Int. SPIN Workshop on Model Checking of Software. Berlin: Springer. 2000. p. 73-92. (Lecture Notes in Computer Science). https://doi.org/10.1007/10722468_5