An effective technique for the software requirements analysis of NPP safety-critical systems, based on software inspection, requirements traceability, and formal specification

A thorough requirements analysis is indispensable for developing and implementing safety-critical software systems such as nuclear power plant (NPP) software systems because a single error in the requirements can generate serious software faults. However, it is very difficult to completely analyze system requirements. In this paper, an effective technique for the software requirements analysis is suggested. For requirements verification and validation (V&V) tasks, our technique uses software inspection, requirement traceability, and formal specification with structural decomposition. Software inspection and requirements traceability analysis are widely considered the most effective software V&V methods. Although formal methods are also considered an effective V&V activity, they are difficult to use properly in the nuclear fields as well as in other fields because of their mathematical nature. In this work, we propose an integrated environment (IE) approach for requirements, which is an integrated approach that enables easy inspection by combining requirement traceability and effective use of a formal method. The paper also introduces computer-aided tools for supporting IE approach for requirements. Called the nuclear software inspection support and requirements traceability (NuSISRT), the tool incorporates software inspection, requirement traceability, and formal specification capabilities. We designed the NuSISRT to partially automate software inspection and analysis of requirement traceability. In addition, for the formal specification and analysis, we used the formal requirements specification and analysis tool for nuclear engineering (NuSRS).     

Formal verification of functional properties of a SCR-style software requirements specification using PVS

Industrial software companies developing safety-critical systems are required to use rigorous safety analysis techniques to demonstrate compliance to regulatory bodies. In this paper, we describe an approach to formal verification of functional properties of requirements for an embedded real-time software written in software cost reduction (SCR)-style language using PVS specification and verification system. Key contributions of the paper include development of an automated method of translating SCR-style requirements into PVS input language as well as identification of property templates often needed in verification. Using specification for a nuclear power plant system, currently in operation, we demonstrate how safety demonstration on requirements can be accomplished while taking advantage of assurance provided by formal methods.     

SMV model-based safety analysis of software requirements

Fault tree analysis (FTA) is one of the most frequently applied safety analysis techniques when developing safety-critical industrial systems such as software-based emergency shutdown systems of nuclear power plants and has been used for safety analysis of software requirements in the nuclear industry. However, the conventional method for safety analysis of software requirements has several problems in terms of correctness and efficiency; the fault tree generated from natural language specifications may contain flaws or errors while the manual work of safety verification is very labor-intensive and time-consuming. In this paper, we propose a new approach to resolve problems of the conventional method; we generate a fault tree from a symbolic model verifier (SMV) model, not from natural language specifications, and verify safety properties automatically, not manually, by a model checker SMV. To demonstrate the feasibility of this approach, we applied it to shutdown system 2 (SDS2) of Wolsong nuclear power plant (NPP). In spite of subtle ambiguities present in the approach, the results of this case study demonstrate its overall feasibility and effectiveness.     

Software design specification and analysis technique (SDSAT) for the development of safety-critical systems based on a programmable logic controller (PLC)

This paper introduces a Software Design Specification and Analysis Technique (SDSAT) for safety-critical systems based on a Programmable Logic Controller (PLC). During software development phases, the design phase performs an important role in connecting the requirements phase and the implementation phase, and it is a process of translating software requirements into software structures. In this work, the Nuclear FBD-style Design Specification and analysis (NuFDS) approach was proposed for nuclear Instrumentation and Control (I&C) software. The NuFDS approach is suggested in a straightforward manner for effective and formal software design specification and analysis. Accordingly, the proposed NuFDS approach is composed of a software design specification technique and a software design analysis technique. In addition, for tool support in the design phase, we developed the NuSDS tool based on the NuFDS approach; this tool is used specifically for generating software design specification and analysis for nuclear fields.     

Verification of a primary-to-secondary leaking safety procedure in a nuclear power plant using coloured Petri nets

This paper deals with formal and simulation-based verification methods of a PRImary-to-SEcondary leaking (abbreviated as PRISE) safety procedure. The PRISE safety procedure controls the draining of the contaminated water in a faulty steam generator when a non-compensable leaking from the primary to the secondary circuit occurs. Because of the discrete nature of the verification, a Coloured Petri Net (CPN) representation is proposed for both the procedure and the plant model. We have proved by using a non-model-based strategy that the PRISE safety procedure is safe, there are no dead markings in the state space, and all transitions are live; being either impartial or fair.Further analysis results have been obtained using a model-based verification approach. We created a simple, low dimensional, nonlinear dynamic model of the primary circuit in a VVER-type pressurized water nuclear power plant for the purpose of the model-based verification. This is in contrast to the widely used safety analysis that requires an accurate detailed model. Our model also describes the relevant safety procedures, as well as all of the major leaking-type faults. We propose a novel method to transform this model to a CPN form by discretization. The composed plant and PRISE safety procedure system has also been analysed by simulation using CPN analysis tools. We found by the model-based analysis—using both single and multiple faults—that the PRISE safety procedure initiates the draining when the PRISE event occurs, and no false alarm will be initiated.     

Electronics in nuclear power programme of India—An overview

This paper presents an overview of state-of-the art developments in electronics for nuclear power programme of India. Indigenous activities in instrumentation and control (I&C) in the areas of detector development, nuclear instrumentation, monitoring and control electronics and special sensors paved the way to self-reliance in nuclear industry. Notable among the recent I&C systems developed for 540 MWe reactors are Liquid Zone Control System (LZCS), flux mapping system and advance reactor regulating system. In a nuclear plant, apart from ensuring functional requirements, design of electronics needs to meet high level of reliability, safety and security standards. Therefore, a lot of importance is attached to activities such as design review, testing, operation, maintenance and qualifications of I&C systems. Induction of computer based I&C systems mandated a rigorous verification process commensurate with the safety class of the system as specified in Atomic Energy Regulatory Board (AERB) safety guides. Software reliability is assured by following strict development life cycle combined with zero-defect policy and is verified through verification and validation (V&V) process. Development of new techniques in data transmissions with optical fibres as transmission medium and wireless networks in control systems is being pursued. With new I&C systems, efforts were made to utilize the same hardware and software platforms for various plant applications, i.e., for standardization. Thrust was given to use Field Programmable Gate Arrays (FPGA) and Application Specific Integrated Circuits (ASIC) in order to improve the reliability of system by reducing component count. It has become imperative to develop modern contemporary solutions like ASICs, HMCs, System on Chip (SOC) and detector mounted electronics and towards that various ASICs and HMCs have been developed in-house to meet the challenges.     

Gray wolf optimizer approach to the reliability‐cost optimization of residual heat removal system of a nuclear power plant safety system

To ensure the safety of nuclear power plants (NPPs), nuclear regulatory agencies set technical specifications (TSs). TSs define the safety‐related operational measures and specify essential requirements and set specific limitations that is necessarily be followed by a nuclear industry to meet the requirements for the safety of an NPP. One of the important bases for the setting of TSs is the estimates of the availability and reliability of various systems and costs associated with an NPP. In this work, authors have presented a framework based upon a hodiernal nature‐inspired metaheuristic called multiobjective gray wolf optimizer (MOGWO) algorithm, which mimic the hierarchal and hunting behavior of gray wolves (Canis lupus), for technical specifications optimization of residual heat removal system (RHRS) of an NPP safety system. The efficiency of MOGWO in optimizing the TSs is demonstrated by comparing its results with a very popular swarm‐based optimization technique named multiobjective particle swarm optimization (MOPSO).     

Assessment of human–machine interface design for a Chinese nuclear power plant

A nuclear power plant (NPP) is a complex system but requires high reliability. The human–machine interface (HMI) design plays very important role in reactor safety. This paper describes an assessment on HMI design of a Chinese NPP, using a software system named Dynamic Interaction Analysis Support (DIAS). DIAS can give not only quantitative indices for dynamically assessing the HMI design, but also allow modify the values of these indices by taking into account human error probability during specified emergent operation procedures. The operation procedures dealing with postulated accidents and transients recorded from a full-scale plant simulator in the training center of a Chinese NPP were selected as references. According to the results of simulation and analysis, the potential problems in the HMI design and the operation procedures were detected. Suggestions to improve the HMI design and the operation procedures were addressed.     

Automated hazard analysis of digital control systems

Digital instrumentation and control (I&C) systems can provide important benefits in many safety-critical applications, but they can also introduce potential new failure modes that can affect safety. Unlike electro-mechanical systems, whose failure modes are fairly well understood and which can often be built to fail in a particular way, software errors are very unpredictable. There is virtually no nontrivial software that will function as expected under all conditions. Consequently, there is a great deal of concern about whether there is a sufficient basis on which to resolve questions about safety. In this paper, an approach for validating the safety requirements of digital I&C systems is developed which uses the Dynamic Flowgraph Methodology to conduct automated hazard analyses. The prime implicants of these analyses can be used to identify unknown system hazards, prioritize the disposition of known system hazards, and guide lower-level design decisions to either eliminate or mitigate known hazards. In a case study involving a space-based reactor control system, the method succeeded in identifying an unknown failure mechanism.     

System and software safety analysis for the ERA control computer

The European Robotic Arm (ERA) is a seven degrees of freedom relocatable anthropomorphic robotic manipulator system, to be used in manned space operation on the International Space Station, supporting the assembly and external servicing of the Russian segment. The safety design concept and implementation of the ERA is described, in particular with respect to the central computer's software design. A top–down analysis and specification process is used to down flow the safety aspects of the ERA system towards the subsystems, which are produced by a consortium of companies in many countries. The user requirements documents and the critical function list are the key documents in this process. Bottom–up analysis (FMECA) and test, on both subsystem and system level, are the basis for safety verification. A number of examples show the use of the approach and methods used.     

Knowledge verification for fuzzy expert systems

Abstract

The introduction and use of fuzzy logic has strengthened knowledge representation and reasoning capability in expert systems; nevertheless, it also increases the complexity and difficulty of knowledge verification, which is known to be an important issue for building reliable and high performance expert systems. In the past decade, knowledge verification problems, e.g., redundancy, conflict, circularity and incompleteness of knowledge, have been widely discussed from the viewpoint of using binary logic; nevertheless, the issue of verifying fuzzy knowledge is seldom discussed. In this paper, we attempt to detect potential structural errors among fuzzy rules by proposing a fuzzy verification algorithm. Moreover, a system for verifying fuzzy knowledge base has been developed based on the novel approach.     

An analytical approach to quantitative effect estimation of operation advisory system based on human cognitive process using the Bayesian belief network

The design of instrumentation and control (I&C) systems for nuclear power plants (NPPs) is rapidly moving towards fully digital I&C systems and is trending towards the introduction of modern computer techniques into the design of advanced main control rooms (MCRs) of NPPs. In the design of advanced MCRs, human–machine interfaces have improved and various types of decision support systems have been developed. It is important to design highly reliable decision support systems in order to adapt them in actual NPPs. In addition, to evaluate decision support systems in order to validate their efficiency is as important as to design highly reliable decision support systems. In this paper, an operation advisory system based on the human cognitive process is evaluated in order to estimate its effect. The Bayesian belief network model is used in the evaluation of the target system, and a model is constructed based on human reliability analysis event trees. In the evaluation results, a target system based on the operator's cognitive process showed better performance compared to independent decision support systems.     

Proving the correctness of client/server software

Remote procedure calls (RPCs) lie at the heart of any client/server software. Thus, formal specification and verification of RPC mechanisms is a prerequisite for the verification of any such software. In this paper, we present a mathematical specification of an RPC mechanism and we outline how to prove the correctness of an implementation—say written in C—of this mechanism at the code level. We define a formal model of user processes running concurrently under a simple operating system, which provides inter-process communication and portmapper system calls. A simple theory of non-interference permits us to use conventional sequential program analysis between system calls (within the concurrent model). An RPC mechanism is specified and the correctness proof for server implementations, using this mechanism, is outlined. To the best of our knowledge this is the first treatment of the correctness of an entire RPC mechanism at the code level.     

A computational model for knowledge-driven monitoring of nuclear power plant operators based on information theory

To develop operator behavior models such as IDAC, quantitative models for the cognitive activities of nuclear power plant (NPP) operators in abnormal situations are essential. Among them, only few quantitative models for the monitoring and detection have been developed. In this paper, we propose a computational model for the knowledge-driven monitoring, which is also known as model-driven monitoring, of NPP operators in abnormal situations, based on the information theory. The basic assumption of the proposed model is that the probability that an operator shifts his or her attention to an information source is proportional to the expected information from the information source. A small experiment performed to evaluate the feasibility of the proposed model shows that the predictions made by the proposed model have high correlations with the experimental results. Even though it has been argued that heuristics might play an important role on human reasoning, we believe that the proposed model can provide part of the mathematical basis for developing quantitative models for knowledge-driven monitoring of NPP operators when NPP operators are assumed to behave very logically.     

Manufacturing knowledge verification in design support systems

This paper identifies the need for a verification methodology for manufacturing knowledge in design support systems; and proposes a suitable methodology based on the concept of ontological commitment and the PSL ontology (ISO/CD18629). The use of the verification procedures within an overall system development methodology is examined, and an understanding of how various categories of manufacturing knowledge (typical to design support systems) map onto the PSL ontology is developed. This work is also supported by case study material from industrial situations, including the casting and machining of metallic components. The PSL ontology was found to support the verification of most categories of manufacturing knowledge, and was shown to be particularly suited to process planning representations. Additional concepts and verification procedures were however needed to verify relationships between products and manufacturing processes. Suitable representational concepts and verification procedures were therefore developed, and integrated into the proposed knowledge verification methodology.     

Application of genetic algorithms to fault diagnosis in nuclear power plants

A nuclear power plant (NPP) is a complex and highly reliable special system. Without expert knowledge, fault confirmation in the NPP can be prevented by illusive and real-time signals. A new method of fault diagnosis, based on genetic algorithms (GAs) has been developed to resolve this problem. This NPP fault diagnosis method combines GAs and classical probability with an expert knowledge base. By assessing the state of the NPP, the GA colony undergoes a transformation that produces an individual adapted to the NPP's condition. Experiments performed on the 950 MW full size simulator at the Beijing NPP simulation training center show that this method has comparative adaptability to diagnose signals and faults changed with time, imperfect expert knowledge, illusive signals and other phenomena.     

Synthesis of a web-based dimensional verification system for styling processes

A design methodology is proposed for a web-based collaborative system applicable to styling processes in the distributed environment. By using the developed system, design reviewers of new products are able to confirm geometric shapes, inspect dimensional information of products through measured point data and exchange views with other design reviewers on the internet. Functional requirements for the design of this web-based dimensional verification system are suggested. ActiveX-server architecture and OpenGL plug-in methods using ActiveX controls realize the proposed system. Visualization and dimensional inspection of the measured point data are conducted directly on the web; conversion of point data into a CAD file or VRML form is not required in the styling process. Dimensional verification results and design modification ideas are uploaded through markups and/or XML files during the collaboration processes. The XML files, allowing information sharing on the web, are independent of the platform. It is possible to diversify the information sharing capability among design collaborators. The validity and effectiveness of the developed system are confirmed by case studies.     

Application of artificial neural networks to nuclear power plant transient diagnosis

A study on various artificial neural network (ANN) algorithms for selecting a best suitable algorithm for diagnosing the transients of a typical nuclear power plant (NPP) is presented. NPP experiences a number of transients during its operations. These transients may be due to equipment failure, malfunctioning of process systems, etc. In case of any undesired plant condition generally known as initiating event (IE), the operator has to carry out diagnostic and corrective actions. The objective of this study is to develop a neural network based framework that will assist the operator to identify such initiating events quickly and to take corrective actions. Optimization study on several neural network algorithms has been carried out. These algorithms have been trained and tested for several initiating events of a typical nuclear power plant. The study shows that the resilient-back propagation algorithm is best suitable for this application. This algorithm has been adopted in the development of operator support system. The performance of ANN for several IEs is also presented.