论文标题
K-ST：PLC的结构化文本语言的正式可执行语义
K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs
论文作者
论文摘要
可编程逻辑控制器（PLC）负责许多工业系统（例如在制造业和公共基础架构中）中自动化过程控制，因此确保它们正确，安全地运行至关重要。大多数PLC以结构化文本（ST）等语言进行编程。但是，缺乏正式的语义使得很难确定其翻译人员和编译器的正确性，而这些语义与供应商不同。在这项工作中，我们开发了K-St，这是K框架中ST的正式可执行语义。 K-St是根据IEC 61131-3标准和PLC供应商手册定义的，是一种高级参考语义，可用于评估不同ST实现的正确性和一致性。我们通过执行从GitHub提取的509个ST程序来验证K-St，并将结果与现有的商业编译器（即Codesys，CX-Programmer和GX Works2）进行比较。然后，我们应用K-ST来验证开源OpenPLC平台的实现，将几个测试程序的执行进行比较，以发现编译器中的五个错误和九个功能缺陷。
Programmable Logic Controllers (PLCs) are responsible for automating process control in many industrial systems (e.g. in manufacturing and public infrastructure), and thus it is critical to ensure that they operate correctly and safely. The majority of PLCs are programmed in languages such as Structured Text (ST). However, a lack of formal semantics makes it difficult to ascertain the correctness of their translators and compilers, which vary from vendor-to-vendor. In this work, we develop K-ST, a formal executable semantics for ST in the K framework. Defined with respect to the IEC 61131-3 standard and PLC vendor manuals, K-ST is a high-level reference semantics that can be used to evaluate the correctness and consistency of different ST implementations. We validate K-ST by executing 509 ST programs extracted from Github and comparing the results against existing commercial compilers (i.e., CODESYS, CX-Programmer, and GX Works2). We then apply K-ST to validate the implementation of the open source OpenPLC platform, comparing the executions of several test programs to uncover five bugs and nine functional defects in the compiler.
