KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification
Programmable logic controllers (PLCs) are special purpose computers designed to perform industrial automation tasks. They require highly reliable control programs, particularly when used in safetycritical systems such as nuclear power stations. In the development of reliable control programs, formal...
Main Authors: | , , , , , |
---|---|
Format: | Article |
Language: | English |
Published: |
IEEE
2019-01-01
|
Series: | IEEE Access |
Subjects: | |
Online Access: | https://ieeexplore.ieee.org/document/8620198/ |
id |
doaj-a130e6215ea943258ad3ed311261d8e2 |
---|---|
record_format |
Article |
spelling |
doaj-a130e6215ea943258ad3ed311261d8e22021-08-30T23:00:15ZengIEEEIEEE Access2169-35362019-01-017145931460210.1109/ACCESS.2019.28940268620198KST: Executable Formal Semantics of IEC 61131-3 Structured Text for VerificationYanhong Huang0https://orcid.org/0000-0003-2102-4303Xiangxing Bu1Gang Zhu2Xin Ye3Xiaoran Zhu4Jianqi Shi5Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, ChinaNational Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai, ChinaNational Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai, ChinaNational Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai, ChinaNational Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai, ChinaHardware/Software Co-Design Technology and Application Engineering Research Center, East China Normal University, Shanghai, ChinaProgrammable logic controllers (PLCs) are special purpose computers designed to perform industrial automation tasks. They require highly reliable control programs, particularly when used in safetycritical 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.https://ieeexplore.ieee.org/document/8620198/Formal verificationK frameworkoperational semanticsprogrammable logic controller |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Yanhong Huang Xiangxing Bu Gang Zhu Xin Ye Xiaoran Zhu Jianqi Shi |
spellingShingle |
Yanhong Huang Xiangxing Bu Gang Zhu Xin Ye Xiaoran Zhu Jianqi Shi KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification IEEE Access Formal verification K framework operational semantics programmable logic controller |
author_facet |
Yanhong Huang Xiangxing Bu Gang Zhu Xin Ye Xiaoran Zhu Jianqi Shi |
author_sort |
Yanhong Huang |
title |
KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification |
title_short |
KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification |
title_full |
KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification |
title_fullStr |
KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification |
title_full_unstemmed |
KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification |
title_sort |
kst: executable formal semantics of iec 61131-3 structured text for verification |
publisher |
IEEE |
series |
IEEE Access |
issn |
2169-3536 |
publishDate |
2019-01-01 |
description |
Programmable logic controllers (PLCs) are special purpose computers designed to perform industrial automation tasks. They require highly reliable control programs, particularly when used in safetycritical 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. |
topic |
Formal verification K framework operational semantics programmable logic controller |
url |
https://ieeexplore.ieee.org/document/8620198/ |
work_keys_str_mv |
AT yanhonghuang kstexecutableformalsemanticsofiec611313structuredtextforverification AT xiangxingbu kstexecutableformalsemanticsofiec611313structuredtextforverification AT gangzhu kstexecutableformalsemanticsofiec611313structuredtextforverification AT xinye kstexecutableformalsemanticsofiec611313structuredtextforverification AT xiaoranzhu kstexecutableformalsemanticsofiec611313structuredtextforverification AT jianqishi kstexecutableformalsemanticsofiec611313structuredtextforverification |
_version_ |
1721184924582543360 |