Runtime Verification of Program Organization Units in Safe Programmable Logic Controller Systems

Programmable Logic Controllers (PLCs) play an essential role in industrial automation by managing complex safety-critical processes. Ensuring the safety and correctness of PLC programs is important, particularly in safety-critical interconnected systems. Although formal verification methods, such as model checking, provide correctness guarantees, they are often impractical for complex PLC systems owing to scalability limitations. Additionally, increased system interconnectivity introduces potential security vulnerabilities. This paper proposes a Runtime Verification (RV) approach to enhance the safety, security, and correctness of PLC programs. Our solution enables users to synthesize runtime monitors through a Graphical User Interface (GUI), using C as the specification language. The synthesized monitors verify the execution of Program Organization Units (POUs) without altering the PLC control flow, ensuring compliance with the defined safety properties. By integrating RV into the PLC execution, we are able to provide a lightweight and adaptable approach for detecting violations and ensuring system reliability. We report preliminary experimental results on the application of our solution to two different case studies, one on a Piped Gas Control Subsystem (PGCS) and the other on a Temperature Control System (TCS). In both cases, we show that the computational and memory overhead introduced by our synthesized monitors is negligible, thus demonstrating that program organization units can still run effectively while being monitored.