Semantics and Analysis of PLC System


Introduction

A programmable logic controller (PLC) is commonly used in industrial control systems, and Structured Text (ST) serves as an imperative programming language for developing PLC software. Given the safety-critical nature of PLC applications, it is essential to formally verify PLC programs. A rewriting-based formal semantics for ST has been introduced for this purpose. In this project, we propose a bounded model checking technique for PLC ST programs, leveraging the rewriting-based semantics. We employ rewriting modulo SMT to symbolically examine LTL properties of ST programs concerning sequences of inputs and outputs, which may be infinite. The effectiveness of our approach has been demonstrated through a case study involving traffic lights.

Although recent developments in executable semantics for PLC ST have been made, existing approaches often overlook the complexity of multitasking and preemption. This project introduces executable semantics for PLC ST that supports preemptive multitasking. The formal analysis of multitasking programs, however, faces the challenge of state explosion. To address this issue, this project also presents state space reduction techniques to enhance the model checking of multitasking PLC ST programs.

Members

References

The following items show the publication from this project:

Software Verification Laboratory, Department of Computer Science of Engineering, POSTECH
77 Cheongam Rd, Nam-gu, Pohang, Gyeongbuk, 37673 Korea.