Atomic Condition Coverage Analysis for Structured Text Based Programmable Logic Controller (PLC)

Programmable Logic Controller (PLC) programmers frequently need to employ formal techniques, such as model checking, to verify the logic of PLC programs. Structured Text (ST) is a high-level programming language for PLCs, and the current practice involves translating an ST program into an equivalent input language (e.g., C or Symbolic Model Verifier (SMV) code) for testing with a model checker. However, this translation process is labour-intensive and often error-prone. It is a new technique to evaluate the coverage of an ST program, and there is also no commonly accepted structural test coverage criteria for ST programs. In this paper, we present the development of an effective atomic condition coverage criterion for testing high-level Structured Text programs. The proposed testing method establishes a grammar, transforms ST programs into Python, and then assesses whether all conditions in an ST program are attainable. We annotate the ST code with artificial runtime errors within the conditional scope. Subsequently, we employ the ANTLR tool to generate the parser and lexical analyzer from the grammar, and a Python code iterates through the ST code line by line, converting it into Python code. We perform a runtime analysis of the Python code and trace it back to the original ST code.