CN115398358B 用于分析可编程逻辑控制器程序的方法 （三菱电机株式会社）

2022.09.16PCT/JP2020/04930220WO2021/199552EN2021.10.07公开了一种PLC程序分析方法，其中，程序(PROG)被转换(TRANS1)成逻辑框架中的程序模互锁属性(IntProp)相结合的所述属性由自动求解器(SMT)验证。如果属性(Prop)的对置是可满述模型的错误初始配置(IniConf)。利用所述模型错误初始配置(IniConf)模拟模型的执行(EXE)，并且记录所述模型模拟的错误中间配置(AST_IntConf)直到所述属性违反。所述原始程Lad_IntConf)是从所述模型的错误初始配置(IniConf)和所述模型模拟的错误中间配置(AST_IntConf)导出的并且被显示。提供了一种2够满足的程序模型的输入和内部存储器值的一组反例，或者如果所述一组属性总是满足，始程序的错误初始配置和错误中间配置；并且显示所述程序错误初始配置和错误中间配3所述原始程序转换为所述程序模型的步骤包括静态单一赋值变换的定对所述一组属性的先验条件，基于所述一组属性的先验条件执行对所述一组属性的验解器来验证与互锁属性关联的所述一组属性解器来验证与互锁属性关联的所述一组属性解器来验证与互锁属性关联的所述一组属性行时执行根据权利要求1至19中的任一项所述计算机程序的存储器和连接至所述存储4[0001]本发明涉及用于分析以IEC61131_3标准中描述的语言编写的程序的方法和装[0004]PLC配备了根据输入和内部存储器的值计算输出的软件，因此取代了硬接线继电[0008]第一种类型涉及单一测试和集成测试，并且包括检查不同组件的行为和常见交关于程序的功能规范的错误。功能测试评估程序是否符合功能规范中指定的要求被编写。得完全不可能保证选定的测试在生产环境中覆盖程序的所有可能执行。在测试阶段之后，5什么所考虑的初始配置会在程序的某个点导解规范并编写不相关代码的实现时间并且在测试人员可能会由于对规范的误解导致设置[0019]本公开的一个目的是提供一种用于详尽地验证可编程逻辑控制器程序的解决方[0021]将可编程逻辑控制器程序类型的原始程序转换为[0023]至少从所述程序模型和预定义的语言形式化来确定与所述原始程序的内部变量[0024]通过自动求解器验证与从规范模型获得的互锁属性相结合的所述一组属性的可的一组反例以及可满足所述属性对置的内部存储器值，或者如果始终满足所述一组属性，[0025]将反例转换为所述程序模型的错误初始配置，所述初始配置包括输入和内部存[0026]用所述程序模型的错误初始配置模拟程序模型的执行，并从执行开始到所述属6[0027]将所述程序模型的错误初始配置和所述程序模型模拟的错误中间配置转换为所[0029]更具体地，本发明提供了一种解决方案来明确表达PLC程序的功能规范并完全自证PLC程序的功能规范的通常基于测试的方法相反，通常基于测试的方法不能测试根据所[0033]本发明除了保证PLC程序的执行安全性和合理性之外，还提供了一种验证功能规范的解决方案。该方法检测由程序员在一阶逻辑中表达的运行时间错误或功能规范违反，7[0040]用户规范描述了PLC程序预期执行的功能，并且通常在根据所述用户规范开发的语法树还允许存储每个元素在PLC程序中的位置，这对于在程序模型的模拟执行期间检索[0044]第一中间步骤，将所述程序模型错误初始配置转换为对应于抽象语法树的错误[0045]第二中间步骤，计算具有所述相应初始配置的抽象语法树并检索与抽象语法树[0046]抽象语法树表示是有利的，因为它允许生成无法通过简单执行PLC程序获得的中8[0052]本发明还旨在提供一种存储根据本发明的计算机程序并且使计算机执行如上定及[0057]本发明的其它特征和优点从以非限制性示例的方式给出并且参考比以上论述的[0075]图1示出了由参考数字10表示并且在PLC程序演绎验证中涉及的一组示例性步这组步骤表示分析和验证PLC程序的方法的实现的全9范模板。更准确地说，功能规范模板与PLC程序使用的设备的选择一起被显示在图形界面[0084]该方法的第一步骤(TRANS1)是转换步骤，包括将PLC程序(PROG)转换为程序模型[0085]所述PLC程序PROG可在以下称为PLC的可编程逻辑控制器上执行。PLC能够存储和PLC语言原语的预定义模型化，以将PLC程序(PROG)转换为以逻辑框架表示的程序模型[0091]程序模型(PMOD)最好用一阶逻辑的逻辑框架来表示。一阶逻辑是命题逻辑的扩论所基于的语言的语义理论的所有解释或结程序首先被表示为抽象语法树，也称为AST表示或语法树，并且以下简称为首字母缩略词[0098]可以使用AST包含的每个元素的属性和注释等信息来编辑和增强AST。对于PLC程[0104]将用户规范转换为规范模型的第二步骤(TRANS2)有利地将程序模型(PMOD)与预定义的语言形式化(LForm)相结合，以获得与所述程序模型(PMOD)[0110]先验条件(PreCond)表示属性(Prop)固有的潜在假设，并且应该在其执行之前进[0113]为此，该第三步骤(PredT)使用狄克斯特拉最弱先验条件演算来计算所述属性并[0116]对一阶逻辑属性执行狄克斯特拉(Dijkstra)最弱先验条件演算确保这样的计算骤(TRANS2)中获得的规范模型(SMOD)中获得的。所述互锁属性是与模型的属性一起计算的，作为要满足的附加后验条件。因此，使用狄克斯特拉最弱先验条件演算，先验条件[0123]在优选实施方式中，第四步骤由可满足性模理论(SMT)问题的自动定理证明器执行，它可用于证明大量内置逻辑理论及其组合中的一阶公式的有效性或双重地可满足性。[0126]如果在使用SMT求解器计算时满足在第三步骤获得的属性(Prop,IntProp)，则由[0128]该方法的第五步骤将获得的属性反例(PROOFNOK)转换(TRANSB)为模型配置，并换是基于所述预定义语言形式化(LForm)执行的，并且作为程序模型(PMOD)的第三步骤中[0129]所获得的属性反例包括对应于初始(IniConf)和中间(IntCo因为程序模型和演绎验证过程是功能性的。所述初始模型配置(IniConf)包括在开始执行述中间模型配置包括在程序模型(PMOD)的执行开始和所述属性不被满足的模型位置之间行具有从反例中选择的所述初始配置的程序模型(IniConf)来重新计算中间变量(X1，X2，步骤中获得的模型初始配置(IniConf)转换为AST表示的相应初始配置(AST_IniConf)，优[0137]第七步骤(DISP)将模型错误场景转换回PLC程序。AST表示配置(AST_IniConf、AST_IntConf)被转换回PLC程序的相应配置。PLC程序分析方法的第七步骤是以语言为中违反或运行时间错误发生的原因和时间以及如何修复PLC程序的指示。在梯形图编程的特[0138]图6示出了具有二进制值的颜色的错误场景和所述错误场景的整数值的标签。如在第一步骤中添加到程序模型中的错误位置和原因信息提供了与被发现的错误以及如何[01