A Systematic and Bibliometric Review of Formal Methods for Securing Industrial Control Systems and Programmable Logic Controllers (2002-2025)

Industrial Control Systems (ICS) and Programmable Logic Controllers (PLCs) are vital elements of infrastructure charged with the responsibility of managing the physical process of manufacturing systems, energy networks, utilities, and other vital services. These systems are critical to safety and are also getting exposed to networked environments, thus making security assurance a significant research question. In that regard, the use of formal methods has been of great interest, being the mathematically sound means of checking both the security and safety properties of various abstraction layers.

Formal verification is the method that allows demonstrating or disproving whether a program or a system meets its specifications or other desired aspects based on logical arguments [1].

In industrial control applications, both safety and security requirements are often included in the specifications, and formal methods are especially suited to this area. Formal approaches to risk reduction, through the provision of exhaustive and sound verification guarantees, alleviate risks related to software defects, malicious attacks, and unintended behaviors of the system.

A rich assortment of formal methods can be used when industrial cyber-physical systems are modelled as hybrid systems, which are discrete control logic and continuous physical dynamics. They are model checking, satisfiability modulo theories (SMT) solving, non-standard analysis, process calculus, concolic testing, and theorem proving [2-5]. Although they have theoretical strength, one of the primary problems of methodology implementation is the inability to establish correct formal models that adequately describe the interactions of PLC programs with the physical processes that occur [3].

The use of formal verification on industrial control logic has been subject to development over the last three decades. Initial experience with the verification of control logic programs proved that the latter was indeed possible, with more recent work indicating that PLC software is specific to formal verification because it is written in graph-based programming languages, it runs in a deterministic manner, and its code is not particularly large ‎[1, 6]. There are two primary paradigms of formalization, in general, in this field: model checking, which uses temporal logic and state-space exploration to prove the correctness of systems, and theorem proving, which interprets systems in the form of logical formulas and demonstrates their correctness by using deductive reasoning [1]. These methods have been used in numerous studies that have been able to increase the safety and security of PLC programs ‎[7].

Parallel to verification-oriented methods, security-by-design models have also become a proactive method of securing ICS. Instead of applying retrofitting to address the deployed security mechanisms, these frameworks incorporate security requirements into the system development cycle and use the published industrial standards to inform the design of secure PLC applications.

A prominent one is that the IEC 61499 function block standard is utilized to enable security-conscious PLC development. This practice allows the designers to mark important parts in the design phase that are then automatically secured by appropriate security measures at the deployment stage ‎[8]. These are achieved with the help of IEC 61499 Service Interface Function Blocks (SIFBs), which incorporate Intrusion Detection and Prevention System (IDPS) functionality, which is automatically compiled into the application ‎[8].

Even though formal verification and industrial cybersecurity have been the focus of more and more studies, there are still a number of limitations associated with the existing literature. The literature is typically dedicated to particular verification methods or particular industrial standards without giving a clear picture of the various formal methods to provide security to ICS and PLC systems. Moreover, numerous studies focus on theoretical points and fail to explicitly discuss the practical issues regarding scalability, model complexity, as well as its application to the real-world industrial environment.

Thus, the goal of this paper is to deliver a systematic and bibliometric review of security strategies using formal methods in the context of ICS and PLCs. The aim of the analysis will be to examine the development of the research trends, the most common formal techniques applied, and to pinpoint the key challenges and gaps in the research in this field.

The rest of this paper will be structured in the following way. Section 2 is the research methodology with the choice of the database, establishment of keywords, and the inclusion and exclusion criteria. Section 3 provides the findings of the bibliometric analysis, including the description of the retrieved data, the development of the scientific production, citation and impact analysis, the major publication sources, geographical distribution of research production, and the analysis of the keywords, including word clouds, thematic systematization, trend topics, co-occurrence networks, and international collaboration patterns. In Section 4, we have presented a comparative analysis of formal-method-based security solutions of the ICS and Programmable Logic Controllers (PLCs).

Section 5 concentrates on the formal-method-based anomaly detection methods for ICS and PLC systems, whereas Section 6 provides a summary and comparison of formal tools that are employed in securing the industrial control environment. The key issues and constraints are addressed in Section 7. Lastly, the paper concludes with a discussion of future work in Section 8.

3.1 Overview of retrieved data

Figure 2 gives an overall summary of the key bibliometric measures, calculated based on the quantified dataset, consisting of 800 articles published between the years 2002 and 2025 and in 226 different sources, such as journals and conference proceedings. It is a corpus varied with 1,709 authors and reflecting the working as a group aspect of studying the subject area, which is formal methods applied to the security of ICS and PLCs. Notably, no single-authored publications were identified, indicating that research in this domain is predominantly conducted through collaborative efforts. The consideration of a scientific growth rate of 5.15 percent per year is an indication of a constant and sustained interest in research in the field of study, as it indicates the rising significance of security and formal verification of ICS. The estimate of international co-authorship is 20.25%, and it is important to note that the average number of co-authors per document is relatively high (6.7), which indicates that the field is multidisciplinary and it may need skill at the level of cybersecurity, control engineering, and formal methods. The data has a total of 5,178 cited sources, which represent a good theoretical base and a high level of dependence on previous academic literature. Moreover, the mean document age of 10.2 years and mean of 12.5 citations per document indicate that the field incorporates the well-established foundational research with a steady flow of new contributions and makes formal-method-based security of ICS and PLCs an active and dynamic field of research.

Figure 2. Descriptive statistics of publications, which were extracted between 2002 and 2025

3.2 History of the development of scientific production

As it is presented in Figure 3, there was a comparatively low level of scientific production connected with the application of formal methods to assure ICS and Programmable Logic Controllers (PLCs) in the early years of the research period, the period between 2002 and around 2008. It can be seen thereafter that a gradual increase is followed by moderate growth between 2009 and 2014. Since 2015, the pattern of publications has started showing a stronger increasing trend, as this signifies the increasing research topic owing to the increasing issues with cybersecurity in industrial and cyber-physical settings.

The sharpest increase is after 2016, which is associated with the growing interest in Industry 4.0, the industrial connection, and the necessity of the strict security guarantee methods. The peak of the trend is expected to be observed in 2023-2024, which means that the research activity on formal-method-based security measures in ICS and PLC systems will be at its peak. The fact that the numbers have been slightly reduced in 2025 is probably because the year has not been completely published.

Figure 3. Annual publication count of journal articles

3.3 Citation and impact analysis

Figure 4 illustrates how the popularity of the field of formal method-based security in ICS and PLC systems has changed over the years in terms of the number of citations. Some definite peaks can be found in the late 2000s and once more in the late 2019-2020, which can be attributed to the influence of some underlying and modern research. This is because the number of new publications is decreasing over the last few years, mostly because of the little time left before the newly published articles can gather many citations.

Figure 4. Citation and impact analysis

3.4 Mapping affiliation authors, sources, and thematic domains

Figure 5 shows the mapping of authors’ affiliations and sources of publications and thematic field in the subject matter of formal method-based security of ICS PLCs. The number shows that academic and research institutions are very active in producing leading journals and conference proceedings, including Lecture Notes in Computer Science, IEEE Access, and major IEEE conferences. The primary themes of focus are PLCs, model checking, formal verification, ICS, and network security, which show a strong resonance between the institutional research knowledge, publication sites, and the prevailing research interests in the field.

Figure 5. Mapping affiliation authors, sources, and thematic domains

3.5 Core publication sources

Figure 6 points out core publication sources in the area of security in ICS and PLCs by means of the formal approach. Lecture Notes in Computer Science is the most prolific with 65 publications, and this is an indicator of the powerful influence of the research based on conference-oriented research in this field.

It is preceded by IFAC-Papers Online (28 documents), IEEE International Conference on Emerging Technologies and Factory Automation (ETFA) (16 documents) that confirm the significance of automation and industrial informatics forums. Different IEEE journals and conference papers, such as IEEE Access, IEEE Transactions on automation science and engineering, and IEEE International Conference on industrial informatics, are also sources of literature. Such a distribution shows a peer-reviewed conference and high-impact journal literature-dominated research landscape, the interdisciplinary character of ICS and PLC security research, which cuts across formal methods, automation, and industrial informatics.

Figure 6. Core publication sources

3.6 Scientific output by country

Figure 7 shows how publications are distributed by country using the respective author, differentiating between single-country publications (SCPs) and multiple-country publications (MCPs). It has been revealed that China, the United States, and Germany have the highest contributions to the scientific output concerning formal-method-based security in the field of ICS and PLCs. The compensation of the publications on the countries is a significant percentage of global collaboration; it demonstrates that there is an active involvement in the global research networks. Other European nations such as France, Italy, Sweden, and the United Kingdom are also showing commendable contributions despite a decreased volume. On the whole, the presence of MCPs in a number of countries indicates the increased significance of international research cooperation in the development of formal verification and cybersecurity systems to protect ICS, which allow the exchange of knowledge and innovation on a global scale.

Figure 7. Countries and international collaboration of the corresponding author

3.7 Word cloud representation

Figure 8 presents the prevailing themes of research on formal method-based security of ICS and PLC systems. The keywords like “Programmable Logic Controllers”, “model checking”, and “formal verification” are placed in the central position, and such keywords as “Petri nets” and “network security” are used to show the emerging and complementary directions of research.

Figure 8. Word cloud representation

3.8 Thematic systematization of research on formal-method based security of Industrial Control Systems and Programmable Logic Controller systems

Table 2 presents a summary of the thematic distribution of the publications that deal with the security of ICS and PLCs via formal methods. Those results indicate that the most noticeable research theme is PLC verification (25.0%), then model checking methods of the ICS/SCADA and Petri-net based methods, each taking 19.0% of the literature. The automata and state machine-based approaches (15.0%), and formal method-supported intrusion and anomaly detection (16.0%) based approaches are also significant research topics. Conversely, the topics connected with testing and reconfiguration constitute a less significant portion (6.0%), which points to new directions that can become more important as the requirements of industrial security continually advance.

Table 2. Thematic distribution of publications on formal method-based security for Industrial Control Systems (ICS) and Programmable Logic Controllers (PLCs) systems

3.9 Trend topics

Figure 9 shows how the research topics in the area of formal-method-based security in industrial systems have changed over the years. During the initial years of the research time frame (2002-2008), the research primarily involved the study of basic notions of formal languages, automata theory, and the synthesis of control systems, which formed the conceptual basis of the subsequent progress in formal verification.

The direction of research changed during the years 2010-2016, when greater attention was paid to the use of formal techniques in industrial settings. It became dominated by topics like Petri nets, model checking, PLC verification, and SCADA systems as an expression of growing interest in the application of formal verification to ICS.

Since 2018, there has been a shift in the area of research, with the focus on the issues of cybersecurity. Cyber-attacks, network security, embedded systems, and system-on-chip architecture also became more important issues, and this indicates that there was increased concern over the protection of industrial infrastructures against cyber attacks.

The trend of the research tends to shift towards a growing interest in cyber-physical security and industrial systems in the framework of Industry 4.0 in the last few years (2022-2024). This change is undergoing an increasing convergence of the ICS and advanced communication systems, and intelligent manufacturing space. Such trends suggest a recent global trend to security assurance of ICS, and more and more emphasis is given to formal verification, intrusion detection, and resilience of connected ICS and PLC environments to the changing threats of Industry 4.0.

Figure 9. Trend topics

3.10 Co-occurrence network of keywords

Figure 10 displays a network of co-occurrence of keywords, indicating that these words are at the center of the literature: it is evident that “Programmable Logic Controllers”, “model checking”, and “formal verification” are core ideas of the literature. Tightly-knit families around “ICS”, “SCADA systems”, and “Petri nets” point to the high degree of integration between formal-modelling and industrial security issues. Less central, though more applicable clusters, such as “network security”, “embedded systems”, and “system-on-chip”, indicate the incorporation of cyber, software, and hardware viewpoints in securing contemporary industrial and cyber-physical systems.

In this section, we will have a comparative analysis of the major anomaly detection techniques used on ICS and PLCs using formal methods. They are based on formal models, which are used to model normal system behavior and identify any deviation that can be a sign of system faults or cyber-attacks.

Table 5 gives an overview of the representative anomaly detection methods that apply to formal methods of industrial control settings. The methods reviewed use formal modelling models like Petri nets, timed automata, reachability analysis, and process mining to describe the normal operation patterns and detect the abnormal behaviors. These methods counter a large spectrum of attacks, such as control logic manipulation, network-based attacks, timing attacks, and cyberspace anomalies in cyber-physical interactions. Formal methods allow identifying deviations in the expected system behavior by modelling the expected system behavior, which in turn can be malicious activity or faults in the operation of the system.

Table 5. Formal methods- based anomaly detection approach for Industrial Control Systems (ICS) and Programmable Logic Controllers (PLCs) systems

Figure 13. Formal-method-based anomaly detection framework for Industrial Control Systems (ICS)

In general, the findings that are summarized in Table 5 reveal that formal models can offer interpretable, state-aware, and proactive anomaly detection mechanisms in industrial settings. The analysis, however, also identifies that there are several practical limitations such as the accuracy of system models, scalability issues, and the complexity of implementing formal verification methods in large-scale industrial infrastructures.

Figure 13 shows a conceptual structure of anomaly detection in ICS and PLCs based on formal methods. It starts with the gathering of system data, logs, network traffic, and sensor measurements that the industrial control environment creates.

They are then analyzed with the help of formal system models, i.e. Petri nets, timed automata, reachability analysis, and process mining systems that are applied to the model, and check the anticipated system behavior.

The system behavior observed is then checked against the one that is to be experienced as per the formal model to measure deviations that may arise. Lastly, the anomaly detection phase detects events that are abnormal, which can be related to control logic attacks, network intrusion, timing anomalies, or cyber-physical faults of the industrial process. To demonstrate how formal models can be applied to the detection of anomaly in an industrial setting, Figure 13 shows a conceptual model of the key steps of the overall detection process.

The bibliometric analysis reveals that the research on the topic of formal security verification of the ICS and PLCs is dominated by model checking and Petri-net-based technology. Nonetheless, the review of the literature indicates that much of the available literature is primarily theoretical validation instead of a large-scale application in industries. This observation correlates with established drawbacks of the formal verification methods, especially the state-space explosion problem and scalability concerns, in the context of their implementation in the complex industrial settings. Nevertheless, even with solid mathematical backgrounds, there are multiple technical and operational difficulties with the practical use of the formal methods for the security of ICS and PLC systems. Among the most outstanding ones, there is the discrepancy between the research-based validation and the actual industry practice. The fact that most ICS security architectures have been tested by simulation or in controlled experimental settings, formal approaches are seldom used to model and prove working industrial infrastructures and are still mostly limited to research [43]. Besides this gap of implementation, there is also another significant constraint that relates to the scope of verification. The majority of the current solutions are mostly concerned with the software analysis of the PLC source code, and do not address other essential areas like compile-time bugs, binary-level attacks, and program behavior during runtime. Thus, a number of types of attacks that take place during the execution of the program, as well as at the firmware level, cannot be properly identified with the help of the existing formal verification methods [44]. Furthermore, formal models using specifications often impose a large amount of manual work on the domain expert, or even direct access to PLC code, which is not readily accessible in the industrial world. Although data-driven and machine-learning-informed methods are more flexible and adaptable, they are not always interpretable and do not have formal guarantees, which restricts the application of such methods in safety-critical industrial processes [45]. Moreover, scalability is also a significant challenge since the growing complexity of the modern ICS networks only intensifies the problem of state-space explosion, which becomes computationally challenging to exhaustively verify. Formal verification techniques also necessitate specialized experience that is usually limited in an operational setting where formal verification techniques are integrated into industrial operational workflow.

To address these issues, recent research trends show that there has been increased interest in integrating formal methods of verification with smart and information-rich methods in an effort to eliminate the shortcomings of the strictly formal models. More specifically, formal verification combined with artificial intelligence has become one of the promising areas of research that can enhance scalability and adaptability in industrial cybersecurity. Hybrid methods seek to use the mathematical assurances of formal methods and take advantage of the learning and pattern recognition of artificial intelligence to identify complex or shifting patterns of attack. The other research direction is of importance as it focuses on the automation of formal model generation, which is a process that is known to be expensive and time-consuming. Machine learning algorithms could be useful in deriving formal models of PLC programs, forming state machines out of network traces, and creating Petri-net-like forms out of sensor and actuator logs. These automated model extraction methods may enormously cut the manual labor needed in the system specification as well, as speed up the verification process in the real-life industry setup. Moreover, the combination of runtime verification and adaptive anomaly detection mechanisms is also discussed as a topic of recent research. Formal models in this case can be used to specify valid system states as well as safety constraints, whereas AI-based detectors can be used to monitor real-time operation data and detect abnormal behavior. The runtime enforcement mechanisms may be activated when the two mechanisms confirm the occurrence of anomalous activity in order to stop unsafe system actions. Such an overlay verification approach enhances the strength, readability, and safety of ICS as well as the formal correctness assurances. The latest trends in anomaly detection methods in ICS and PLC environments also indicate these new areas of research. Specifically, a few of the studies suggest anomaly detection tools that examine the structures of the PLC control logic and the operational data to determine any malicious code modifications or abnormal control flows present in industrial settings [40]. As an example, Lee et al. [40] presented a control-logic-based anomaly detection model that can detect malicious changes to the PLC program through learning the structural properties of control logic instructions. Equally, there are other works that discuss more sophisticated hybrid detection constructs that integrate machine learning or deep learning models with formal system behavior modelling to enhance the accuracy of detection in industrial settings [46]. Other recent strategies also seek to solve the problem of small industrial datasets by synthesizing synthetic ICS time-series data on generative models to enhance the performance of anomaly detection [41]. Furthermore, other proposals are made on the use of ensemble and unsupervised learning techniques to identify abnormalities in PLC-based industrial processes without the need for labeled attack datasets [47]. In addition to these methods, more recent studies also cover how formal verification tools like model checking and Petri-net-based models may be combined with runtime monitoring tools to detect cyber-physical anomalies during execution [48]. Additional new frameworks can also integrate digital twin models and causal reasoning algorithms to have a more informed perspective of system behavior and false alarm rate when identifying attacks in cyber-physical industrial contexts [42]. On the whole, all these changes testify to the shift that the research environment has passed in the trend topic analysis shown in Figure 9. The number shows that there has been an increased interest in industrial cybersecurity, anomaly detection, formal verification, and cyber-physical system security in the past decade, although the research activity has grown significantly after 2020. This tendency is manifested in the growing sophistication of the modern industrial infrastructure and the expansion of the necessity to have scalable security systems, uniting formal approaches with intelligent monitoring systems.