Design And Implementation Of A Prototyping Tool For Automatical Verification Of PLC Programs For SPS4PLC

Programmable logic controller(PLC)is an embedded device widely used in industrial con-trol field.It is often used to implement the control logic of safety-critical systems,such as nu-clear power plant,transportation,and medical equipment.These systems have extremely high requirements for the correctness and reliability of the software.At present,PLC program devel-opment mainly relies on personal experience,and requirements description errors and program design errors are inevitable.SPS4PLC is derived from the specification pattern language SPS.It is a specification lan-guage dedicated to describing PLC control systems.It can accurately describe the requirements of PLC control systems in a manner close to natural language.SPS2 PLC is a tool that automat-ically generates PLC programs from SPS4 PLC specifications.However,the correctness of the generation process has not been confirmed by the machine.In order to verify the correctness of programs generated by the SPS2 PLC tool,this thesis tries to verify if PLC programs is consis-tent with the specifications described in the SPS4 PLC language by model checking.The main work of this thesis is as follows:(1)This thesis gives a formal semantic model of a PLC IL language programs,which focuses on the semantic rules of the setting methods of the scan period length and the semantic rules of the timer.On this basis,the translation method from PLC programs to time automata model is given.(2)This thesis proposes a modeling method that does not fix the length of the scan period.Through theoretical and experimental analysis,it is found that this modeling method of the unfixed scan period can not only effectively detect the timing properties,but also improve the efficiency of verification.However,this modeling method may cause the verification of the programs that should have passed the verification to fail in some cases,so this thesis adopts the method of secondary verification.That is,the model with an unfixed scan period is preferred for verification,and the model with a fixed scan period length is used for re-verification when the verification fails.(3)This thesis proves the consistency of the two behaviors from the level of operational se-mantics.(4)Aiming at the problem of state space explosion,this thesis introduces the specific imple-mentation scheme of influence cone reduction in the work of this thesis.(5)This thesis uses the observer method to transform SPS4 PLC into a verifiable TCTL logic formula.(6)Finally,this thesis designs and implements PLCVerifier,an automatic PLC verification tool for SPS4 PLC.Application PLCVerifier can quickly verify the correctness of programs au-tomatically generated by SPS2 PLC.This article uses PLCVerifier to verify the implemen-tation patterns of all the SPS4 PLC scope patterns,and finds three inconsistencies between the implementation patterns and SPS4 PLC semantics,and gives corrections.For various PLC systems,the programs generated by SPS2 PLC were verified,and it was found that SPS2 PLC can generate correct programs under the condition that there is no circular de-pendency in the given specification.In addition,this tool can also verify PLC programs developed in other ways.