Formal Verification Of Real-Time Properies On PLC Programs Using Coq

PLCs(Programmable Logic Controllers)are embedded devices widely used in safety-related industrial control.These areas require high reliability,but traditional simulation and testing methods can not fully guarantee the correctness of the program,so strict formal methods must be used to verify them.There is no systematic method to prove the temporal and real-time specifications descripted in temporal logic in the existing work.This paper presents a set of verification rules to help users proof temporal and real-time properties in a deductive way.The main work of this paper is as follows:(1)An operational semantics of a subset of ST language is given,which covers most of the important language features such as scan cycle,TON timer,etc.The TON timer is modeled according to 10-ms timer in Siemens S7-200 series PLC,which is more accurate and practical than other existing models.On this basis,a extended Hoare logic can be used to prove the single-cycle properties,which describes the effect of the program by executing a scan cycle.(2)A set of verification rules for temporal properties is proposed,by which the multi-cycle properties described by linear temporal logic are derived from the single-cycle properties.These rules mainly aims at two kinds of common properties in PLC program: security and self-holding properties.The verification of security properties has been fully studied.In this paper,the existing methods are migrated to the cyclic sampling system such as PLC.Self-holding structure is a basic programming idiom in PLC program.This paper presents a formal specification and verification method for this kind of structure.(3)A set of verification rules for real-time properties is proposed.Since the timer is the basis of realizing real-time function in PLC,the real-time logic MTL is used to describe their behavior in various situations;then the verification rules are used to prove that the typical timer program satisfies these specification;combined with other temporal properties,the real-time properties of the whole program is deduced.(4)The interactive theorem prover Coq is used to implement all the verification procedures,including formal semantics,specification language and verification rules.To reduce the proof burden,some automatic proof tatics aimed at single-cycle properties and timer properties are devoloped.Using the above method,several common program fregments are verified.The results show that this method can effectively deal with typical PLC programs and detect some errors.