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


Mader, A.H. and Brinksma, H. and Wupper, H. and Bauer, N. (2001) Design of a PLC Control Program for a Batch Plant - VHS Case Study 1. European Journal of Control, 7 (4). pp. 416-439. ISSN 0947-3580

open access
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.
Item Type:Article
Additional information:Imported from DIES
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page