Formal Semantics and Analysis of PLC Systems


Introduction

Programmable Logic Controllers (PLCs) are widely used in industrial control systems to interface with physical environments through sensors and actuators. Given their role in safety-critical domains, the correctness of PLC software is crucial, and formal verification becomes essential. However, the behavior of a complete PLC system involves several complex components: cyclic execution of Structured Text (ST) programs, real-time interaction with physical environments, task preemption under multitasking settings, and communication between networked controllers.

This research aims to develop a unified and realistic formal semantics that captures the complete behavior of PLC systems. Our approach covers the formalization of the ST programming language, support for symbolic and bounded model checking, semantics for preemptive multitasking with state space reduction, and integration of continuous environment dynamics and networked communication. Through executable semantics, tool support, and scalable verification techniques, our framework offers a foundation for analyzing real-world PLC systems in industrial settings.

Semantics of PLC ST

We define K semantics of PLC ST. K is a rewriting-based framework for defining the semantics of programming languages. In K, program states are specified as multisets of nested cells, called configurations. Each cell represents a component of the program state, such as environments and stores. The cell structure for PLC ST is shown below.

PLCs exhibit cyclic behavior where a ‘scan cycle’ consists of input, execution, and output stages. During the input stage, it reads values from sensors (e.g., temperature, water level) and stores them in the program variables. Based on these values, the programs are executed in the execution stage. Finally, the output variables’ values are reflected in the actuators (e.g., motor speed, pump switch). We formalize this cyclic behavior and integrate it into the LTL model checking analysis procedure, whereas formal studies focus on the single execution of PLC programs.

Another important distinction from previous work is that we do not assume specific input values. At this point, we do not know what values can be read from the environment; we virtually assume that ‘any’ values of a specified range can be read. This necessitates the need for a symbolic semantics with SMT variables as program values. To include these behaviors in our semantics, we extend the cell structures with the following cells.

Bounded Symbolic Model Checking and STbmc Tool

We employ rewriting modulo SMT to symbolically examine LTL properties of ST programs concerning sequences of inputs and outputs. A model checking problem is encoded into reachability to an error state. LTL properties are ‘flatten’ to a propositional formula over the input and output stream elements. The following shows a Maude search command to verify the LTL property φ.

We develop ‘stbmc’ tool that takes PLC programs and specification files and performs model checking. The following shows the specification file format and the command line output of the tool. If the given LTL property holds, ‘test succeeded’ is printed. If not, it shows a counterexample.

Semantics and Analysis of Multitask PLC

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.

Under multitask PLC setting, various scenarios can occur from the same initial state. The following diagram shows two possible scenarios (among many) that may have different outcome. Our semantics is meant to capture all possible scenarios. The following cells are added or modified to the cells originally proposed. (1) time denotes the current time; (2) active denotes the identifier of the currently running program; (3) interval has a map from program identifiers to their intervals; (4) pQueue contains a priority queue of tasks that are ready to run according to time and interval; and (5) futureTS contains tasks that are not ready. By moving task objects from pQueue and futureTS back and forth, we can naturally define the multitask PLC behaviors.

To resolve state explosion, we propose ‘time-abstraction’ and ‘partial order reduction’ techniques. The main idea of time-abstraction is to express time abstractly with a time interval that represents an infinite number of time points. We have adopted the classic ample set based partial order reduction approach to our system. The graph below shows the time comparison of state space exploration time before and after time abstraction. The points at 3600 represent timeout.

Physical Dynamics and Communication of PLCs

Existing formal verification techniques focus on individual PLC programs in isolation, often neglecting interactions with physical environments and network communication between controllers. We present a unified formal framework that integrates discrete PLC semantics, networked communication, and continuous physical behaviors.

The environment interacts with the programs by sensing and actuation at the beginning of every scan cycle. The environmental state, such as temperature and switch position, is included in each PLC’s attributes. We define ‘tick’ rule that rules the time evolution of the system, which updates the environmental states.

PLC supports several function blocks that conduct inter-PLC communication, which includes ‘CONNECT’ for connection establishment, ‘USEND’ for asynchronous sending data, and ‘URCV’ for asynchronous receiving data. The behavior of each communicating function block is implemented in PLC ST format, with special communication functions defined in rewrite rules.

Using this integrated semantics, we can verify properties of well-defined networked industrial control systems such as chemical plants with water tanks, railed vehicle controllers, and so on.

Ongoing Work

This ongoing work is motivated by the observation that multitask PLC semantics and the semantics for physical dynamics and inter-controller communication are largely orthogonal. Our goal is to develop a unified semantics that incorporates both preemptive multitasking and cyber-physical interaction within a single framework. As part of this effort, we are conducting a case study involving PLC-controlled vehicles that must avoid collisions while navigating toward designated destinations.

Contact

References

The following items show the publication from this project: