Automatic verification of temporal and timed properties of control programs

• Main Author: Zoubek, Bohumir
• Published: University of Birmingham 2004
• Subjects: 005.14
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.419737

Control system programs are usually validated by testing prior to their deployment. Unfortunately, testing is not exhaustive and therefore it is possible that a program which passed all the required tests still contains errors. We propose to use automatic verification, which can establish whether given properties are true or not through exhaustive exploration of the model, in addition to validation through testing. This thesis defines a framework for modelling and verification of control programs. A subset of ladder diagram program elements, given by the IEC 61131-3 standard, is supported. The models can be automatically extracted from ladder diagrams and converted to timed automata. The timed automata models are then verified using the real-time model checker Uppaal. The properties to be verified are expressed in temporal logic and can be timed. Abstraction techniques based on program slicing and variable dependency graphs are employed to tackle the well known state-space explosion problem which often results in the verification becoming infeasible. The framework proposed in the thesis was implemented in Java as a proof-of concept software tool that can serve as a back-end in the control programmers' toolbox. The tool was then used to analyse two case studies given as ladder diagrams. The first case study concerned a pumping line unit with four properties, one of which was timed. In this case, all properties were successfully verified. The second case study consisted of a gas burner control program. The program was found to contain errors that were discovered automatically, and then corrected after analysing diagnostic traces produced by the Uppaal model checker. After modifications, the program was shown to satisfy the original properties. Statistics giving model sizes and verification time are presented for each case study for a range of abstraction techniques. We believe that the work presented in the thesis successfully demonstrates that automatic verification can substantially enhance current validation procedures for control programs.