Paper Info
Title
Kst: Executable Formal Semantics Of Iec 61131-3 Structured Text For Verification
Abstract
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.
Year
DOI
Venue
2019
10.1109/ACCESS.2019.2894026
IEEE ACCESS
Keywords
Field
DocType
Formal verification, K framework, operational semantics, programmable logic controller
IEC 61131-3,Programming language,Computer science,Structured text,Semantics of logic,Distributed computing,Executable
Journal
Volume
ISSN
Citations 
7
2169-3536
0
PageRank 
References 
Authors
0.34
0
6
Name
Order
Citations
PageRank
Yanhong Huang14910.56
Xiangxing Bu200.34
Gang Zhu312718.75
Xin Ye411.71
Xiaoran Zhu5173.22
Jianqi Shi65712.50