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 opti-mal 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 ap-proach was to see how much could be achieved here using the standard model checking environment of SPIN/Promela. As the symbolic calcu-lations of real-time model checkers can be quite expensive it is interest-ing 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.