Research On Formal Methods For Verifying Instruction List Program

With the rapid development of computer and network technology, and theincreasing social demand, the national requirements for the automation application inindustry are being strengthened. As a very important automation technology,programmable logic computers (PLCs) provide great help for enterprises, especiallyin the transition from traditional relay control systems to numerical control systems.However, the increasing production accidents warn us that the reliability of theautomatic control procedure can not be ignored.Due to the reliability requirements, the academic circles have developed a lot ofresearches on the control program verification in recent years. There is a greatweakness in the traditional methods, which relay on the programmer’s experience toavoid logic mistakes and can not guarantee the reliability of programs. To overcomethis shortcoming, formal verification methods gradually come into the vision ofresearchers. The formal verification method is mainly divided into two categories thatare the deductive verification and model checking. Compared to the deductiveverification, the model checking is automatic. Therefore, a method is proposed on theformal verification of PLC instruction list in this paper:1. The algorithm is proposed to translate PLC instruction list (IL) programs toPetri nets;2. The system specifications are described by compute tree logic formulas;3. NuSMV is used to check Petri-net model of an IL program and its computetree logic formulas;4. The method is presented to correct the target progam according the checkingresults.This paper aims to improve the reliability of instruction list programs, and toreduce the potential security risks in actual production according the above methods.The methods may provide effective help for improving the automatic control systemsof enterprises.