基于符号约束的PLC程序正确性验证

摘要：

符号约束描述了程序中的变量关系,被广泛运用于模型检测、符号执行等程序的静态分析方法中.将符号约束应用于可编程逻辑控制器(PLC)程序的正确性验证,能够发现程序中的逻辑错误.人工计算符号约束不仅冗杂枯燥,而且错误率高.针对语句表形式的PLC程序,提出一种基于符号约束的正确性验证方法,通过分析PLC源代码的控制流及数据流,构造程序的控制流图并将其转换为静态单赋值形式的三地址码,最后使用迭代计算的方法求出每个变量的符号约束.

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

所属期刊栏目：44

分类号：TP312(计算技术、计算机技术)

在线出版日期：2018-01-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：348-352