TY - JOUR
T1 - KST
T2 - Executable Formal Semantics of IEC 61131-3 Structured Text for Verification
AU - Huang, Yanhong
AU - Bu, Xiangxing
AU - Zhu, Gang
AU - Ye, Xin
AU - Zhu, Xiaoran
AU - Shi, Jianqi
N1 - Publisher Copyright:
© 2019 IEEE.
PY - 2019
Y1 - 2019
N2 - Programmable logic controllers (PLCs) are special purpose computers designed to perform industrial automation tasks. They require highly reliable control programs, particularly when used in safety-critical systems such as nuclear power stations. In the development of reliable control programs, formal methods are "highly recommended" because the correctness of intended programs can be mathematically proven. Formal methods generally require precise semantics indicating how the program behaves during execution. However, for PLC programming languages, formal semantics is not always available rendering the application of formal methods highly challenging. In this paper, we present formal operational semantics of structured text, a widely used PLC programming language. The semantics is based on the ST language specification provided by IEC 61131-3, a generally acknowledged international standard for PLCs. We define the formal semantics in K which is a rewriting-based semantic framework and has been successfully applied in defining the semantics of many general-purpose programming languages such as C [1] and, Java [2]. We validate our formal semantics by testing examples from the standard and then apply the semantics on the verification of control programs for PLCs.
AB - Programmable logic controllers (PLCs) are special purpose computers designed to perform industrial automation tasks. They require highly reliable control programs, particularly when used in safety-critical systems such as nuclear power stations. In the development of reliable control programs, formal methods are "highly recommended" because the correctness of intended programs can be mathematically proven. Formal methods generally require precise semantics indicating how the program behaves during execution. However, for PLC programming languages, formal semantics is not always available rendering the application of formal methods highly challenging. In this paper, we present formal operational semantics of structured text, a widely used PLC programming language. The semantics is based on the ST language specification provided by IEC 61131-3, a generally acknowledged international standard for PLCs. We define the formal semantics in K which is a rewriting-based semantic framework and has been successfully applied in defining the semantics of many general-purpose programming languages such as C [1] and, Java [2]. We validate our formal semantics by testing examples from the standard and then apply the semantics on the verification of control programs for PLCs.
KW - Formal verification
KW - K framework
KW - operational semantics
KW - programmable logic controller
UR - https://www.scopus.com/pages/publications/85061752986
U2 - 10.1109/ACCESS.2019.2894026
DO - 10.1109/ACCESS.2019.2894026
M3 - 文章
AN - SCOPUS:85061752986
SN - 2169-3536
VL - 7
SP - 14593
EP - 14602
JO - IEEE Access
JF - IEEE Access
M1 - 8620198
ER -