The transition from analog to digital instrumentation and control systems in nuclear power plants introduces increased complexity, and functionality and consequently new types of risks. Systems Theoretic Process Analysis (STPA) aims to uncover losses caused by inadequate control measures between system elements and could therefore help identify control flaws also in Instrumentation and control (I&C) systems. Our objective is to assess the method's effectiveness in the context of a nuclear power plant's digital feedwater control system use case. We highlight the completeness of the hierarchical control structure of the use case, as a substantial part of the analysis relies on its content. The perspective of STPA viewing safety as a control problem offers valuable insights into the instrumentation and control use case. Altogether more than 140 unsafe control actions and 400 loss scenarios were identified originating from 18 control actions. STPA generates numerous unsafe control actions and loss scenarios but lacks inherent prioritization. The absence of a distinction between important and minor hazards treats all findings equally in terms of criticality for safety requirements and system design considerations. As a result, we tested the risk priority number approach and recognized its utility in screening and prioritizing these findings. This proves beneficial when allocating resources for safety considerations in digital instrumentation and control systems within the nuclear domain.

Model checking is a powerful formal verification method. However, due to the complexity of instrumentation and control (I&C) system logics-even in critical applications like nuclear power plant safety systems-the challenge of state space explosion means that the analyses cannot always be performed in reasonable time. In compositional verification, this challenge is overcome by reasoning over the system subcomponents sepa-rately, and then resolving proof claims for the composite system as a whole. In this paper, I present my experiments with OCRA, a tool for the verification of contract requirement. Together with the model checker nuXmv, OCRA can be used for compositional model checking. My industrial case study relates to three legacy I&C systems of the Finnish Olkiluoto nuclear power plant, about to be renewed using (mostly) software-based logic. I concretize the challenges in verifying complex nuclear I&C logics, prove the capabilities of OCRA, and discuss the practical limitations.

Formal verification methods like model checking can provide mathematical proofs of design correctness, so their use is justified in applications where safety or reliability requirements are high. A key challenge for the wider adoption of model checking is the effort and expertise needed in formalizing functional requirements into verifiable properties. A particular challenge in specifying formal properties for industrial instrumentation and control (I&C) logics is accounting for the sequencing and timing issues that arise from, e.g., the dynamic behavior of the plant being controlled. In this paper, we evaluate different visual property specification languages that are aimed at making formal methods more accessible. We have collected 3923 formal properties from practical model checking projects in the nuclear and rail traffic industries and identified the most commonly occurring types of properties. Based on the sample data, a real-world example logic, and our practical experience, we identify requirements for a user-friendly property specification language most suited for our specific domain of industrial I&C.

We present an approach for suggesting possible fixes to an overall I&C nuclear architecture during its design phase. Despite the I&C architecture, in our case, being represented with an ontology, we do not aim to change the properties of an ontology per se. Instead, we focus on the subset of ABox triples that do not contain terminological elements in either subject, predicate, or object parts. Such a subset we call the design artifacts. When the ontology is filled with the design artifacts, the analyst runs the check of non-functional requirements using SPARQL queries. The requirements associated with the queries that returned results do not hold. The goal of the current work is to provide support for the next stage when the analyst has to change the design artifacts so that the queries no longer return results. Our method is based on representing the results of queries as graphs, intersecting them, and finding the minimal changes that prevent the results from being mapped on their (or other) queries.

Obfuscation is a process of transforming a program into an equivalent version which is harder to understand and reverse-engineer. Little attention has been paid to obfuscation techniques for programs written for programmable logic controllers (PLC). However, there is no reason to assume that an attacker would not be interested in hiding malicious payload into a PLC program before it is compiled to machine code.In this paper, I present five techniques for obfuscating IEC 61131-3 Function Block Diagram (FBD) programs. Four of the techniques are specific to the graphical representation of FBD. I then evaluate the applicability of each technique by experimenting with different PLC programming tools. I prove that at least four of the techniques are practically applicable, and demonstrate features that some tools successfully use to prevent abuse. Stricter rules, if implemented in IEC 61131-3, would prevent some of the techniques listed.

We present an approach for suggesting possible repairs for the control logic of I&C systems implemented in the form of function block diagrams (FBDs) during the design phase. Each FBD has a set of functional requirements formulated using linear temporal logic (LTL). To ensure the correctness of the implementation, an FBD is translated into SMV, the language of the NuSMV model checker, which verifies the model against its properties. If a property does not hold, NuSMV generates a counterexample. In previous works, we developed methods on visual counterexample explanation using both, the failing LTL formula and the FBD itself. The current work continues in this direction and utilizes the results of the counterexample explanation to suggest fixes to the FBD considering the failed properties and the whole set of requirements. We propose three strategies for fixes generation and experiment on the examples of the logic from the nuclear domain.

Formal verification by means of model checking avails in discovering design issues of safety systems at the early stages. However, a significant amount of time and effort is required to decipher its results and localize the failure, especially in complex logic. This work continues our previous study on the visual explanation of failure traces and introduces change-based causes. Additionally, inspired by the types of properties that revealed model failures in projects of VTT in the Finnish nuclear industry, we define a new form of explanation – a hybrid influence graph. The new approach was implemented in a tool called Oeritte and evaluated using two practical examples of failures in nuclear instrumentation and control systems.

Nuclear power plants have many different instrumentation and control (I&C) systems. Together, these systems (and their various dependencies) form the overall I&C architecture, which needs to fulfill the principle of defence-in-depth. The safety systems need to be sufficiently independent from the normal operation systems to avoid common cause failure.Semantic Web technologies use formal conceptual models— ontologies—to associate meaning with unstructured data. The knowledge base is built on named graphs, allowing complex queries with reasoning. The results are based on more than just statistical patterns.In this paper, we demonstrate the use of an OWL ontology to represent engineering knowledge about overall nuclear I&C architectures. We show how, using flexible SPARQL queries, we can then analyse the different dependencies between the I&C systems. We have built a public case study based on a proposed pressurised water reactor type. We detected several potential design issues, which suggests the approach could improve nuclear safety and support design work.

For over a decade, model checking has been successfully used to formally verify the instrumentation and control (I&C) logic design in Finnish nuclear power plant projects. One of the practical challenges is that the model checker NuSMV forces the user to abstract the way analog signals are processed in the model, which causes extra manual work, and could mask actual design issues. In this paper, we experiment with the newer tool nuXmv, which supports infinite-state modelling. Using actual models from practical industrial projects, we show that after changing the analog signal processing to be based on real number math, the analysis times are still manageable. The disadvantage is that certain useful types of formal properties are not supported by the infinite-state algorithms. We also discuss the nuclear industry specific features of I&C programming languages, which cause significant constraints on domain-specific formal verification method and tool development.

Despite being one of the most reliable approaches for ensuring system correctness, model checking requires auxiliary tools to fully avail. In this work, we tackle the issue of its results being hard to interpret and present OERITTE, a tool for automatic visual counterexample explanation for function block diagrams. To learn what went wrong, the user can inspect a parse tree of the violated LTL formula and a table view of a counterexample, where important variables are highlighted. Then, on the function block diagram of the system under verification, they can receive a visualization of causality relationships between the calculated values of interest and intermediate results or inputs of the function block diagram. Thus, OERITTE serves to decrease formal model and specification debugging efforts along with making model checking more utilizable for complex industrial systems.

This paper focuses on the challenges relating to the overall safety instrumentation and control (I&C) architectural design and more specifically the modelling and assessment of nuclear safety I&C systems at architectural level. We focus on the properties relating to Defence-in-Depth principle, mainly on the unwanted interactions between systems of different safety classification. This paper describes the design process of early conceptual overall safety I&C architecture from the modelling point of view and defines the requirements for a model-based approach to support the design and analysis of the design solution. The modelling language selected for the study was Architecture Analysis and Design Language (AADL), an architecture description language, which considers analysis as a goal. In this paper, we review the capabilities of the language for modelling overall safety I&C architectures and as a case study, we model a simplified example architecture of an APR-1400 nuclear power plant using standard AADL components and provide an overview of the analysis capabilities of the OSATE tool for checking Defence-in-Depth related requirements.

Model checking methods have been proven to be a valuable asset for identifying undesired behaviour of safety-critical Instrumentation and Control (I&C) logics. Their application in the nuclear domain has been very successful and has triggered significant interest from the safety community. Creating formal models from the diagrams found on paper or from digital formats without the needed semantics is one bottleneck that hinders the adoption of model checking due to costs in time and may introduce errors. This paper proposes a methodology for the creation of formal models from I&C diagrams drawn in generic modelling tools (lacking specific I&C semantics). The generic I&C logic diagram is transformed into an intermediate UML model that in turn can be transformed to other target formats like IEC 61131 PLCopen XML I&C software or NuSMV formal model code. This methodology is demonstrated with a typical example of a trip signal generator application logic. This application logic is drawn in MS Visio, it is transformed to an I&C model in UML with the needed properties for model checking, then to IEC 61131 PLCopen XML and to an input file for the NuSMV model checker.

Certain safety-critical systems, such as nuclear instrumentation and control (I&C) systems, must be ensured to be correct. One of the approaches of doing this is formal verification and, in particular, model checking, which thoroughly examines the state space of the formal model of the system. To make model checking computationally feasible, many simplifying assumptions, often referred to as abstractions, are made. One of such abstractions is the assumption of discrete time. However, when I&C systems are considered working in the real world, where communication delays and failures are possible, this assumption becomes less realistic, calling for the need for richer formalisms. In this paper, using timed automata, we extend our previous model checking approach for nuclear I&C systems to account for continuous time. We apply our approach to a reactor protection system case study and show that continuous-time verification is in general feasible, although proving the satisfaction of certain system properties still remains a computational challenge.

Model checking is a proven, effective method for verifying instrumentation and control system application logics. If a model of the system being verified does not satisfy a specification, the failure scenario is presented to the user as a counterexample trace. Analysis of the counterexample can be time-consuming if the trace is long, the model is large, or the specification is complex. Spurious counterexamples (“false negatives”) often exacerbate the problem. In this paper, we present a method that assists in identifying the root of the failure in both the model and the specification, by animating the model of the function block diagram as well as the LTL property. We also introduce a practical tool for visualizing LTL properties by animation and highlighting of important values based on causality. Using 43 actual design issues identified in practical nuclear industry projects, we then evaluate usefulness of the property visualization and explanation features.

In some fields of industrial automation, such as nuclear power plant (NPP) industry in Finland, thorough verification of systems and demonstration of their safety are mandatory. Model checking is one of the techniques to achieve a high level of reliability. The goal of this paper is practical: we explore which type of model checking - either explicit-state or symbolic - is more suitable to verify instrumentation and control (I&C) applications, represented as function block networks. Unlike previous studies, in addition to the common open-loop approach, which views the controller model alone, we consider closed-loop verification, where the plant is also modeled. In addition, we present a procedure to translate block networks to the language of the SPIN explicit-state model checker.

To facilitate correctness and safety of mission-critical automation systems, formal methods should be applied in addition to simulation and testing. One of such formal methods is model checking, which is capable of verifying complex requirements for the system's model. If both the controller and the controlled plant are formally modeled, then the variant of this technique called closed-loop model checking can be applied. Recently, a technique of automatic plant model generation has been proposed which is applicable in this scenario. This paper continues the work in this direction by presenting two plant model construction approaches which are much more scalable with respect to the previous one, and puts this work into a more practical context. The approaches are evaluated on a case study from the nuclear automation domain.

Formal methods - such as model checking - have definite advantages over more commonplace verification techniques. By providing proof of the analyzed systems' correctness, they are especially useful in domains that are under regulatory supervision, like the nuclear industry. The foremost challenge for wider adoption of model checking is the effort and the expertise required for formalizing functional requirements into verifiable properties. A particular challenge in verifying the application software of industrial process control systems is taking into account the different sequencing and timing issues that arise from, e.g., the dynamic behavior of the plant processes being controlled. In this paper, we review specification languages that are aimed at making formal methods more accessible. We have collected 1079 sample formal properties from practical model checking projects in the nuclear industry, and identified repeatedly occurring property types. We present our findings, and based on the sample data, evaluate the applicability of different approaches on user-friendly property specification.

Formal methods and languages are used to prove the correctness of various industrial systems, especially mission-critical ones. They can also be viewed as a means to provide safety and correctness demonstration to the stakeholders of such systems. In domains such as nuclear power plant engineering, the benefits from structured safety evidences would seem obvious. However, most stakeholders in nuclear power industry are not even familiar with formal notations. As a result, to promote the applications of formal methods in practice, the first step is to make formal specification languages (FSLs) more accessible. With user-friendly FSLs, users can focus on safety requirements rather than on their sophisticated formalization. This paper, as a preliminary work towards an integrated framework supporting transparent safety demonstration, reviews existing approaches applied to facilitate requirements formalization and formal specifications. Moreover, the common features of user-friendly languages and their tool supports are also summarized.

Model checking is a powerful formal verification method that can also be used to evaluate PLC software. A lot of manual work and some expertise are still needed. Proposed methods for automating the process rely on standardised specification languages, but PLC software is often vendor-specific, and the source code for function blocks may not even be available. We propose a toolset for model checking of function block based software. After manually modelling the elementary function block library, the model of any block diagram can be specified with easy-to-use graphical tools. The counterexamples output by the model checker can also be visualised using a “living” function block diagram. Our toolset is based on integrating the popular model checker NuSMV with the open source modelling platform Simantics.

Semantic Web technologies - ontologies in particular - aim at efficient access to heterogeneous, distributed knowledge. However, current ontology languages such as OWL cannot properly address uncertainties, inconsistencies or contradictions. Fuzzy ontologies have been proposed to fix these shortcomings and further enhance information retrieval. The domain of industrial process plants faces many knowledge management challenges. Knowledge in e.g. the form of written reports is stored in different systems, but retrieval is often ineffective and reuse therefore limited. This paper presents an attempt at applying a fuzzy ontology for searching reports of past situations of interest at a process plant. The aim has been to get richer search results from a knowledge base by extending the query with fuzzy neighbour concepts.

To determine the operational situation of a monitored industrial process, an operator needs efficient access to a wide range of information. Measurement data alone does not encapsulate the overall situation, but pieces of information have to be searched from different plant IT systems that unfortunately often have varying interfaces and data formats. Information agent and semantic Web techniques address similar challenges in the context of the Internet by annotating heterogeneous data with formal semantics provided by ontology languages like OWL, and by providing human users with autonomous assistants for information retrieval. This paper presents an agent based concept for process automation that provides operators with easily configured information retrieval and monitoring services, releasing them from tedious data harvesting tasks.

While automation systems can track thousands of measurements it is still up to human process operators to determine the operational situation of the controlled process, particularly in abnormal situations. To fully exploit the computing power of embedded processors and to release humans from simple data harvesting activities, the concept of proactive computing tries to exploit the strengths of both man and machine. Proactive features can be implemented using intelligent agent technology, enabling humans to move from simple interaction with computers into supervisory tasks. Autonomous information agents can handle massive amounts of heterogeneous data. They perform tedious tasks of information retrieving, combining and monitoring on the behalf of their users. This paper presents a multi-agent-based architecture for process automation, which aims to support process operators in their monitoring activities. The approach is tested with a scenario inspired by a real-world industrial challenge.