Programmable logic controllers (PLC), which are widely applied in modern industrial control systems (ICS), work as the controller of sensors and actuators in ICS. These systems require strict correctness, especially for safety-critical systems. Currently, increasingly ICS move to “come online” scenarios to enhance cyber-physical features, but it makes them more vulnerable due to acquiring increased interconnection accompanied by weakening physical isolation. Moreover, with the more complex controlling environment, such as hundreds of more I/O points and more diverse field buses, the incorrect executions of PLC might cause the failure of the overall ICS. In this article, we examine how the security and safety of running PLC could be enhanced in both developing and deploying stages of ICS. We propose a novel application of runtime verification to guarantee the security and safety of real-world ICS. As a variant of temporal logic, PLC past linear temporal logic (PPLTL) is proposed to specify the security and safety properties of PLC. Using PPLTL, we synthesize monitors to improve the PLC program’s security and safety as a partner of testing and static verification. Our monitors provide twofold processing in a nonintrusive manner: One is filtering abnormal input data before invading the original programs, the other is double-checking the output signals before driving the actuators. We use several case studies and benchmarks to demonstrate the efficiency of the approach. The empirical results show that the time overhead and memory occupation are tiny.

Programmable logic controllers (PLCs) are special embedded computers that are widely used in industrial control systems. To ensure the safety of industrial control systems, it is necessary to verify the correctness of PLCs. Formal verification is considered to be an effective method to verify whether a PLC program conforms to its specifications, but the expertise requirements and the complexity make it hard to be mastered and widely applied. In this paper, we present a specification-mining-based verification approach for IEC 61131-3 PLC programs. It only requires users to review specifications mined from the program behaviors instead of model checking for specified specifications, which can greatly improve the efficiency of safety verification and is much easier for control system engineers to use. Moreover, we implement a proof-of-concept tool named PLCInspector that supports directly mining LTL specifications and data invariants from PLC programs. Two examples and one real-life case study are presented to illustrate its practicability and efficiency. In addition, a comparison with the existing verification approaches for PLC programs is discussed.

Programmable logic controllers (PLCs) are special purpose computers designed to perform industrial automation tasks. They require highly reliable control programs, particularly when used in safetycritical 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.

With the development of the industrial control system, Programmable Logic Controllers (PLCs) are increasingly adopted in the process automation. Moreover, many PLCs play key roles in safety-critical systems like nuclear power plants, where robust and reliable control programs are required. To ensure the quality of programs, testing and verification methods are necessary. In this paper, we present a novel methodology which applies model checking to verifying PLC programs. Specifically, we focus on the Structured Text (ST) language which is a widely-used, high-level programming language defined in the IEC 61131-3 standard. A formal model named Behaviour Model (BM) is defined to specify the behaviour of ST programs. An algorithm based on variable state analysis for automatically extracting the BM from an ST program is given. An algorithm based on the automata-theoretic approach is proposed to verify Linear Temporal Logic (LTL) properties on the BM. Finally, a real-life case study is presented.

With rapid technological advances in airborne control systems, it has become imperative to ensure the reliability, robustness, and adaptability of airborne software since failure of these software could result in catastrophic loss of property and life. DO-333 is a supplement to the DO-178C standard, which is dedicated to guiding the application of formal methods in the review and analysis of airborne software development processes. However, DO-333 lacks theoretical guidance on how to choose appropriate formal methods and tools to achieve verification objectives at each stage of the verification process, thereby limiting their practical application. This paper is intended to illustrate the formal methods and tools available in the verification process to lay down a general guide for the formal development and verification of airborne software. We utilized the Air Data Computer (ADC) software as the research object and applied different formal methods to verify software lifecycle artifacts. This example explains how to apply formal methods in practical applications and proves the effectiveness of formal methods in the verification of airborne software.