Design of a PLC Control Program for a Batch Plant - VHS Case Study 1

Angelika H. Mader, Hendrik Brinksma, H. Wupper, N. Bauer

Research output: Contribution to journalArticleAcademicpeer-review

4 Citations (Scopus)
55 Downloads (Pure)

Abstract

This article reports on the systematic design and validation of a PLC control program for the batch plant that has been selected as a case study for the EC project on Verification of Hybrid Systems (VHS). We show how a correct design of the control program can be obtained in an incremental manner using a real-time logical formalism. This is done by systematically strengthening the premise of an implication whose conclusion represents the required behaviour of the plant. The premise specifies the assumptions under which this behaviour is realised. The formal proof of correctness was obtained using formal verification tools. We used both theorem-proving (PVS) and model checking (Spin) as verification strategies. With PVS we could show the correctness of the final implication directly by a semantic embedding of the real-time logic in PVS, but only for a limited operational scenario (a single batch load). With Spin we could show the correctness for all relevant operational scenarios, but only indirectly, viz. on the basis of an abstract verification model (written in Promela). This model was obtained as a straightforward translation of the premise of the final version of the formal design and the PLC code derived from it. We conclude that the judicious use of standard formal methods and tools suffices for the systematic development of correct control programmes for this kind of application.
Original languageUndefined
Article number10.3166/ejc.7.416-439
Pages (from-to)416-439
Number of pages24
JournalEuropean journal of control
Volume7
Issue number4
DOIs
Publication statusPublished - 2001

Keywords

  • IR-66969
  • EWI-937

Cite this

@article{77eb5f6292f049558b20d59e34517307,
title = "Design of a PLC Control Program for a Batch Plant - VHS Case Study 1",
abstract = "This article reports on the systematic design and validation of a PLC control program for the batch plant that has been selected as a case study for the EC project on Verification of Hybrid Systems (VHS). We show how a correct design of the control program can be obtained in an incremental manner using a real-time logical formalism. This is done by systematically strengthening the premise of an implication whose conclusion represents the required behaviour of the plant. The premise specifies the assumptions under which this behaviour is realised. The formal proof of correctness was obtained using formal verification tools. We used both theorem-proving (PVS) and model checking (Spin) as verification strategies. With PVS we could show the correctness of the final implication directly by a semantic embedding of the real-time logic in PVS, but only for a limited operational scenario (a single batch load). With Spin we could show the correctness for all relevant operational scenarios, but only indirectly, viz. on the basis of an abstract verification model (written in Promela). This model was obtained as a straightforward translation of the premise of the final version of the formal design and the PLC code derived from it. We conclude that the judicious use of standard formal methods and tools suffices for the systematic development of correct control programmes for this kind of application.",
keywords = "IR-66969, EWI-937",
author = "Mader, {Angelika H.} and Hendrik Brinksma and H. Wupper and N. Bauer",
note = "Imported from DIES",
year = "2001",
doi = "10.3166/ejc.7.416-439",
language = "Undefined",
volume = "7",
pages = "416--439",
journal = "European journal of control",
issn = "0947-3580",
publisher = "Lavoisier",
number = "4",

}

Design of a PLC Control Program for a Batch Plant - VHS Case Study 1. / Mader, Angelika H.; Brinksma, Hendrik; Wupper, H.; Bauer, N.

In: European journal of control, Vol. 7, No. 4, 10.3166/ejc.7.416-439, 2001, p. 416-439.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Design of a PLC Control Program for a Batch Plant - VHS Case Study 1

AU - Mader, Angelika H.

AU - Brinksma, Hendrik

AU - Wupper, H.

AU - Bauer, N.

N1 - Imported from DIES

PY - 2001

Y1 - 2001

N2 - This article reports on the systematic design and validation of a PLC control program for the batch plant that has been selected as a case study for the EC project on Verification of Hybrid Systems (VHS). We show how a correct design of the control program can be obtained in an incremental manner using a real-time logical formalism. This is done by systematically strengthening the premise of an implication whose conclusion represents the required behaviour of the plant. The premise specifies the assumptions under which this behaviour is realised. The formal proof of correctness was obtained using formal verification tools. We used both theorem-proving (PVS) and model checking (Spin) as verification strategies. With PVS we could show the correctness of the final implication directly by a semantic embedding of the real-time logic in PVS, but only for a limited operational scenario (a single batch load). With Spin we could show the correctness for all relevant operational scenarios, but only indirectly, viz. on the basis of an abstract verification model (written in Promela). This model was obtained as a straightforward translation of the premise of the final version of the formal design and the PLC code derived from it. We conclude that the judicious use of standard formal methods and tools suffices for the systematic development of correct control programmes for this kind of application.

AB - This article reports on the systematic design and validation of a PLC control program for the batch plant that has been selected as a case study for the EC project on Verification of Hybrid Systems (VHS). We show how a correct design of the control program can be obtained in an incremental manner using a real-time logical formalism. This is done by systematically strengthening the premise of an implication whose conclusion represents the required behaviour of the plant. The premise specifies the assumptions under which this behaviour is realised. The formal proof of correctness was obtained using formal verification tools. We used both theorem-proving (PVS) and model checking (Spin) as verification strategies. With PVS we could show the correctness of the final implication directly by a semantic embedding of the real-time logic in PVS, but only for a limited operational scenario (a single batch load). With Spin we could show the correctness for all relevant operational scenarios, but only indirectly, viz. on the basis of an abstract verification model (written in Promela). This model was obtained as a straightforward translation of the premise of the final version of the formal design and the PLC code derived from it. We conclude that the judicious use of standard formal methods and tools suffices for the systematic development of correct control programmes for this kind of application.

KW - IR-66969

KW - EWI-937

U2 - 10.3166/ejc.7.416-439

DO - 10.3166/ejc.7.416-439

M3 - Article

VL - 7

SP - 416

EP - 439

JO - European journal of control

JF - European journal of control

SN - 0947-3580

IS - 4

M1 - 10.3166/ejc.7.416-439

ER -