分析可编程逻辑控制器程序的方法、计算机程序和装置

摘要

公开了一种PLC程序分析方法，其中，程序(PROG)被转换(TRANS)成逻辑框架中的模型(MOD)，从所述模型(MOD)确定属性(Prop)。与用户规范(IntProp)相结合的所述属性由自动求解器(SMT)进行验证。如果属性(Prop)的对立是可满足的，则提供代表模型输入和内部存储器值的反例(PROOF NOK)。反例(PROOF NOK)被转换成所述模型的错误初始配置(IniConf)。利用所述模型错误初始配置(IniConf)模拟(EXE)模型的执行，并且记录所述模型模拟的错误中间配置(AST‑IntConf)直至所述属性违反。所述原始程序(PROG)的错误初始配置和错误中间配置(Lad‑IniConf，Lad‑IntConf)从所述模型的错误初始配置(IniConf)和所述模型模拟的错误中间配置(AST‑IntConf)得到并被显示出来。提供了一种用于执行所述方法的装置。