K-ST: A formal executable semantics of the structured text language for PLCs
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 Struct...
Saved in:
Main Authors: | , , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2023
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/8199 https://ink.library.smu.edu.sg/context/sis_research/article/9202/viewcontent/k_st_structured_text_tse23_av.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-9202 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-92022023-12-12T03:53:35Z K-ST: A formal executable semantics of the structured text language for PLCs WANG, Kun WANG, Jingyi POSKITT, Christopher M. CHEN, Xiangxiang SUN, Jun CHENG, Peng 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 567 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. 2023-09-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/8199 info:doi/10.1109/TSE.2023.3315292 https://ink.library.smu.edu.sg/context/sis_research/article/9202/viewcontent/k_st_structured_text_tse23_av.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University formal executable semantics PLC programming structured text K framework OpenPLC Programming Languages and Compilers Software Engineering Theory and Algorithms |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
formal executable semantics PLC programming structured text K framework OpenPLC Programming Languages and Compilers Software Engineering Theory and Algorithms |
spellingShingle |
formal executable semantics PLC programming structured text K framework OpenPLC Programming Languages and Compilers Software Engineering Theory and Algorithms WANG, Kun WANG, Jingyi POSKITT, Christopher M. CHEN, Xiangxiang SUN, Jun CHENG, Peng K-ST: A formal executable semantics of the structured text language for PLCs |
description |
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 567 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. |
format |
text |
author |
WANG, Kun WANG, Jingyi POSKITT, Christopher M. CHEN, Xiangxiang SUN, Jun CHENG, Peng |
author_facet |
WANG, Kun WANG, Jingyi POSKITT, Christopher M. CHEN, Xiangxiang SUN, Jun CHENG, Peng |
author_sort |
WANG, Kun |
title |
K-ST: A formal executable semantics of the structured text language for PLCs |
title_short |
K-ST: A formal executable semantics of the structured text language for PLCs |
title_full |
K-ST: A formal executable semantics of the structured text language for PLCs |
title_fullStr |
K-ST: A formal executable semantics of the structured text language for PLCs |
title_full_unstemmed |
K-ST: A formal executable semantics of the structured text language for PLCs |
title_sort |
k-st: a formal executable semantics of the structured text language for plcs |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2023 |
url |
https://ink.library.smu.edu.sg/sis_research/8199 https://ink.library.smu.edu.sg/context/sis_research/article/9202/viewcontent/k_st_structured_text_tse23_av.pdf |
_version_ |
1787136835601825792 |