关键词: 可编程逻辑控制器,符号约束,正确性验证,三地址码,静态单赋值

Abstract: Symbolic constraints describe the relations among variables of the program,and they are widely used in static program analysis methods such as model checking and symbol execution.The logic error in the program could be found while applying symbolic constraints to the correctness verification of the programmable logic controller (PLC)program.However,the process of manually computing symbolic constraints is not only cumbersome and boring,but also with high error rates.Aiming at the PLC program in the form of statement list (STL),a verification method based on gene-rating symbol constraint automatic was proposed.By analyzing the control flow and data flow of the PLC source code,the control flow graph of the program is constructed and the source code is converted into three address code in the form of static single assignment.Finally,the iterative method is used to find the symbol constraint of each variable.