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

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.