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.

翻译：可编程逻辑控制器（PLC）负责众多工业系统（如制造业和公共基础设施）中过程控制的自动化，因此确保其正确、安全运行至关重要。多数PLC使用结构化文本（ST）等语言进行编程。然而，由于缺乏正式语义，其翻译器和编译器（各供应商产品各异）的正确性难以验证。本研究在K框架内为ST开发了正式可执行语义K-ST。K-ST基于IEC 61131-3标准及PLC厂商手册定义，是一种高层参考语义，可用于评估不同ST实现的正确性与一致性。我们通过执行从Github提取的509个ST程序，并将结果与现有商业编译器（CODESYS、CX-Programmer和GX Works2）进行对比来验证K-ST。随后应用K-ST验证开源OpenPLC平台的实现，通过比对多个测试程序的执行结果，发现该编译器中存在五个错误和九项功能缺陷。