Verification Of Industrial Control Programs Based On Coq

The correctness and reliability of industrial control systems are of great significance for economic development,personal safety and social stability.A basic problem of industrial control systems is the temporal problem in control.How to automatically generate a program from the temporal specification is a long-term concern in the academic community.In existing work,the temporal specification is usually expressed in terms of linear temporal logic(LTL)and computation tree logic(CTL),and the programs satisfying these specifications are generated by the game technology and model checking techniques on automaton.The generated program often have the worst-case exponential scale which is not practical enough.Matthew B.Dwyer et al.summarized SPS(specification pattern system)which contains 55 patterns that can describe most of the temporal specifications in the industry.This thesis realizes linear-scale program generation from SPS specifcations.PLC(Programmable Logic Controller)is widely used in industrial control systems,this thesis uses PLC language as the target language.The main work of this thesis are as follows:(1)The exact semantic description of SPS: In the FIL(Future Interval Logic)definition provided by the SPS proposer,the FIL definition of two important scope patterns do not apply to common control scenarios.This thesis gives counterexamples,provides new definitions,and demonstrates the full set of FIL definitions for SPS.(2)Coq model of PLC: This thesis gives the definition of syntax and semantics of PLC language in Coq.This definition reflects the semantic effect of the periodic execution mode of PLC program,and provides a basis for the proof based on Hoare logic.(3)PLC program generation: This thesis defines an SPS specification description language based on the basic SPS.The language embodies the various changes that may faced when describing an actual industrial control system using SPS.Using the combinable characteristic of SPS and the control hierarchy relationship,a PLC program generation rule that satisfies this kind of specification is proposed,and the correctness of the rule is proved.It is proved that the program generated by this rule is linear-scale with respect to SPS specification.For some typical industrial control problems,the program generated by the rule is given,and the correctness of the generated results is proved using Coq.