The nuclear safety video display unit (SVDU) is a critical human-machine interface in the nuclear reactor protection system, and its cybersecurity is increasingly challenged by the sector's full digitalization. This paper proposes a novel cybersecurity risk assessment method integrating an attack tree model with the STRIDE threat framework to evaluate the risk status of the nuclear SVDU. The approach innovatively incorporates the latest CVSS4.0 standard to define security attributes (attack cost, technical difficulty, discovery difficulty, and impact) for leaf nodes, which are quantified through hierarchical scoring. Crucially, an objective entropy weighting method is employed to calculate the weights of these attributes, effectively eliminating the subjective bias inherent in traditional expert-dependent methods like FAHP. The risk probability is then propagated from leaf to root nodes based on their dependency relationships. Comparative analysis demonstrates that the proposed method offers a more sensitive and discriminating assessment, identifying critical threats that subjective approaches might overlook and providing a robust, data-driven basis for prioritizing security protection strategies.

The software-based programmable logic controller is an industrial computer widely used to implement safety–critical systems in digital I C of nuclear power plants. As the complexity of future systems increases and demands for flexibility in control and monitor growing, the scale and role of software are becoming more significant, leading to concerns about software reliability. Formal methods are essential for ensuring software reliability in safety–critical domains. In recent years, formal methods have made substantial advancements, resulting in many sophisticated techniques. However, there is a lack of practical guidelines and a systematic solution in the nuclear domain. In this paper, we propose a comprehensive framework that integrates recent technological advancements in formal methods across all aspects of software development, encompassing definition, design, implementation, verification, and operation. Our aim is to establish a complete formal verification technology stack. Additionally, we also present the progress and future plans for a developing prototype software development toolchain that combines model-driven and formal approaches based on this framework.

Ensuring the reliability and safety of safety-critical systems within nuclear power plant hinges upon efficient failure effects analysis. Conventional approaches to failure effects analysis in reactor protection systems encounter notable challenges, including labor-intensive manual analysis and limitations in ensuring comprehensive analysis coverage. To tackle these issues head-on, we introduce a novel methodology termed Failure Effects Analysis on Safety Properties (FEA-SP). Grounded in model checking technology, this method facilitates automated failure analysis processes. By harnessing the exhaustive state space exploration capabilities inherent in model checking, the FEA-SP methodology adopts the safety properties of the system as its granularity and verification focal point. A detailed component-level case study involving a hard logic within the HPR1000 nuclear reactor protection system underscores the efficacy and practicality of the proposed approach, especially in the thorough examination of system spurious actions. The failure effects analysis method delineated in this paper holds broad applicability and serves as a valuable reference for the analysis of failure effects in safety systems.

To ensure the safe, reliable, and stable operation of nuclear power plants, the instrumentation and control (I C) systems of nuclear power plants provide various control, protection, and monitoring methods for the plants processes and equipment. This paper conducts extensive research on literature and data related to the development of domestic nuclear power I C systems. By examining the current usage of I C systems in operational and under-construction nuclear power plants in China, it outlines the evolutionary process—from the initial analog instrumentation with relay-based control, to analog control combined with non-safety digital monitoring, and finally to the gradual adoption of fully digital I C systems, including safety-class systems. Additionally, this paper analyzes the characteristics of modern digital I C systems and summarizes the design principles for nuclear power instrumentation and control. Finally, it explores and forecasts future technological advancements in nuclear power I C systems. By clearly outlining the current applications and providing a detailed analysis of development trends, this paper offers valuable insights for the future growth of the nuclear power I C industry.

Miniature fission ionization chambers are widely used as in-core neutron detectors in nuclear reactors. The high neutron flux in the core imposes stringent requirements on their operational lifetime. This paper proposes a breeder fission ionization chamber by incorporating U-234 into the U-235 coating, enabling U-235 regeneration via the U-234 (n, γ)U-235 reaction as U-235 is consumed. A multi-physics coupled fission ionization chamber model was developed using Geant4 and Garfield++ to systematically investigate the effects of U-234/U-235 mixing patterns (layered/homogeneous) and U-234/U-235 ratios on detector sensitivity and lifetime characteristics. Simulation results show that: The optimal coating thickness is 5 μm, and the optimal mixing pattern is Radial Layered Type-II (U-235 layer encapsulating U-234). Detector sensitivity decreases monotonically with increasing U-234 proportion. A lifetime iterative model based on simulation data demonstrates that adding U-234 to the coating extends detector lifetime to varying degrees across 25 iterations. Higher U-234 proportions flatten the sensitivity-time curve, indicating improved stability. This study provides theoretical guidance for the engineering design of breeder fission ionization chambers.

In the digital era of increasing software complexity, improving the development efficiency of safety-critical software is a challenging task faced by academia and industry in domains such as nuclear energy, aviation, the automotive industry, and rail transportation. Recently, people have been excited about using pre-trained large language models (LLMs) such as ChatGPT and GPT-4 to generate code. Professionals in the safety-critical software field are intrigued by the code generation capabilities of LLMs. However, there is currently a lack of systematic case studies in this area. Aiming at the need for automated code generation in safety-critical domains such as nuclear energy and the automotive industry, this paper conducts a case study on generating safety-critical software code using GPT-4 as the tool. Practical engineering cases from the industrial domain are employed. We explore different approaches, including code generation based on overall requirements, specific requirements, and augmented prompts. We propose a novel prompt engineering method called Prompt-FDC that integrates basic functional requirements, domain feature generalization, and domain constraints. This method improves code completeness from achieving 30% functions to 100% functions, increases the code comment rate to 26.3%, and yields better results in terms of code compliance, readability, and maintainability. The code generation approach based on LLMs also introduces a new software development process and V-model lifecycle for safety-critical software. Through systematic case studies, we demonstrate that, with appropriate prompt methods, LLMs can auto-generate safety-critical software code that meets practical engineering application requirements. It is foreseeable that LLMs can be applied to various engineering domains to improve software safety and development efficiency.

The role of software is crucial for the stable operation of safety-critical systems such as nuclear equipment. In the face of the advancement and complexity of safety-critical software, new challenges are encountered in the design and development of highly reliable software, and new methods and paradigms for software development and verification are urgently needed. Both formal methods and model-driven techniques have gained increasing attention in this field. In response to this demand, combined with the latest technological trends, this paper focuses on three key scientific problems and explores one basic theory and seven key technologies. Additionally, a prototype software platform is developed. Aiming to overcome the technical bottleneck faced by automatic code-generation software for nuclear equipment in modelling, code generation, testing, and verification, we perform the following tasks: overall design and evaluation of automatic code-generation software for nuclear safety control systems, software modelling technology for nuclear safety control and human-machine interactive systems, model analysis and verification technology for safety control systems, and automatic code-generation technology for verified software for safety control systems. Based on this research, we establish a new safety-critical software development and verification method and paradigm. Moreover, we construct a prototype automatic code-generation system for safety control in nuclear equipment, applying verified software and safety-certification technology. With regard to the overall design and evaluation of the software platform, we perform requirements analysis considering specific application scenarios in various fields and construct domain models. We design the architecture of the software platform and examine the key platform technologies and methods to support module development, functional safety, and compliance with standards. It is necessary to solve the scientific problem of the formal method and model-driven fusion theory and develop a novel technology for safety control software code based on the architecture design of a model-based development environment. In software modelling, it is essential to accurately describe the requirements of the target system in the nuclear domain, characterize the control, interaction, and coordination of the target system, realize accurate modelling of the nuclear domain model, and provide a basis for the analysis and verification of the relevant safety properties of the subsequent model, simulation, and code generation. These can be achieved by solving the scientific problems of the formal semantic theory of nuclear control and the human-interaction model and developing two key technologies: enhanced synchronous data flow modelling technology with safety embedded state machines and graphical human-computer interaction configuration technology for nuclear control systems. In terms of model analysis and test verification, the correctness verification of the safety control system model based on formal and simulation methods should be completed. To achieve this, following key technologies should be developed: model correctness checking technology for safety control systems, intelligent generation and accurate testing technology for high coverage test cases, a general high-reliability virtual simulation driver, and automatic execution technology. In terms of code generation, a highly verified code generator should be developed based on formal verification of transformation from the nuclear power control and interaction system modelling language to a domain-specific safe subset of the C language. It is necessary to solve the scientific problem of the reliable construction theory and synchronous data flow model code generator of control systems extended by safety state machines and develop the key technology for formal verification of synchronous data flow language verified code generators based on theorem proof. The main innovations introduced in this study are as follows: First, we present a new method for developing nuclear safety control software based on the integration of formal methods with model-driven development. This approach guarantees both the reliability of the software and the efficiency of its development. We provide a theoretical basis for the abstract transformation from software code to theorems, and also study, deploy, and schedule the construction of the tool chain around formal verification. Second, we extend the state-machine schema to construct a new language (based on the Lustre language) conforming to the synchronous data-flow theory. A complete and accurate description of complex control logic in safety-critical domains such as nuclear power equipment is provided. Third, we propose a verified code generator based on interactive theorem proving and use it to explore and solve the problem of generating high-reliability safety control code. Fourth, we propose a data-driven and intelligent test-case generation method based on machine learning for exploring the correlation between abstract models and software codes. Finally, we describe an integrated development platform for nuclear safety control software that meets high-level quality and safety requirements. It includes model-based design, simulation, verification, code generation, and other functions, providing one-stop solutions for software development in safety-critical areas. The goal of our research is to offer a new and highly reliable method for developing and verifying safety-critical software. Our results have considerable theoretical and practical implications for scientific research and development of industrial software in domains such as nuclear equipment.

Gateway is a protective equipment at the boundary of the nuclear safety-level I&C system. Aiming at the unknown threat across the boundary of information physical space, this paper studies several key technologies of active defense, and constructs the gateway deep secure architecture that can resist multilevel and multi-dimensional complex attacks. Firstly, the systematic control mechanism of the gateway is constructed, which mechanism includes access control for data flow, IP whitelist at network layer, function code whitelist at application layer, IP/MAC binding and the isolation mechanism of chip’s external ports. Secondly, based on the domestic trust root, the trusted chain from bootloader to the upper-layer application is built to guarantee the secure startup of the embedded system, and the key application processes are measured periodically and verified dynamically during the running process. Based on the above, from building equipment embedded trusted system environment to its security functions, a set of active security defense mechanisms of the gateway equipment sare formed, which enhances the security of the system and improves the information security protection n capability of the equipment.

核电厂的工控网络结构复杂、设备众多,且大部分采用商业秘密的私有通信协议.通信效率和通信质量是常见的系统故障原因.为解决私有通信协议难以测试的问题,通过研究核电厂工控网络私有协议的特征、应用场景和通信的质量属性,采用嵌套的类型-长度-数据(TLV)报文描述技术,提出一种通用的工控网络私有通信协议的测试方法.该方法具有灵活度高、适用范围广、自动化程度高等特点,满足了通信质量的测试要求.该方法结合物理层的硬件适配,可用于核电厂工控网络中不同工控设备、不同私有协议的通信质量测试,有效提高网络运行过程中的安全性和稳定性.

The safety-class (1E) digital control system (DCS) of nuclear power plant characterized structural multiple redundancies, therefore, it is important to quantitatively evaluate the reliability of DCS in different degree of backup loss. In this paper, a reliability evaluation model based on T-S fuzzy fault tree (FT) is proposed for 1E DCS of nuclear power plant, in which the connection relationship between components is described by T-S fuzzy gates. Specifically, an output rejection control system is chosen as an example, based on the T-S fuzzy FT model, the key indicators such as probabilistic importance are calculated, and for a further discussion, the T-S fuzzy FT model is transformed into Bayesian Network(BN) equivalently, and the fault diagnosis based on probabilistic analysis is accomplished. Combined with the analysis of actual objects, the effectiveness of proposed method is proved.

作为核反应堆测量系统的重要组成之一,堆外核测量系统能够实时连续测得反应堆物理参数.核电站堆外核测量数字仪表控制系统的设计需要采用模块化的方法来提高设计效率,以提升设备的可靠性和可维护性.设计了堆外核测量系统的模块化构建方案.该方案以基础模块为基础,由源量程、中间量程、功率量程三个部分构建了整个系统.在此基础上,设计了堆外核测量系统机柜.该机柜能够接收探测器的信号,经处理后将计算结果和设备状态等综合信息发送至其他系统.在不同工况下,综合各项鉴定标准的机柜通过了功能性能试验、长期稳定性试验、堆上测试和鉴定试验.电磁兼容试验、环境试验和抗震试验结果证明,该方案能够在核电仪控设备中批量化应用,并且有利于实现堆外核测设备的数字化.

Information is key to the process of diagnosis, so it is necessary to understand how information amount may influence human performance. The current study investigated this issue through an experiment where participants diagnosed an accident in a simulated nuclear power plant. The amount of accessible information and the times of making judgments were manipulated. The results showed that increasing the amount of accessible information led the participants to seek more and think shallower, and thus decreased diagnostic accuracies, whereas no significant effects were found for multiple judgement times. The authors argue that the disadvantages of more accessible information could be attributed not simply to 'information overload', but partly to the diagnosticians' unwise choice of information processing strategies. The findings imply that system designers should restrain the ever-growing amount of information while users should make more efficient use of information rather than take in more.Practitioner summary: Current research on diagnosis by humans was mostly limited to outcome performance. This study empirically investigated factors influencing its detailed process. The results showed that increasing accessible information amount impaired both process and outcome performances.

Formal methods are required for the automatic generation of codes to ensure that the code generated by the compiler can be applied to nuclear power instrument and control systems and thus minimize the errors introduced by the compiler during the compilation of synchronous data-flow languages. This study uses the theorem proving tool Coq to formally define the syntax, semantics, and translation algorithms involved in the translation phase of the master-node input structure of the synchronous data-flow language from Lustre to Clight and completes the formal proof of the translation algorithm. It is shown that this formalized compiler can generate credible target code that is consistent with the behavior of the source code, and meanwhile, the generated target code can well satisfy the implementation specifications of nuclear power instrument and control systems.

Humans are not very good at assessing their own performance, and usually exhibit over-confidence. Little effort has been done to investigate how and how well diagnosticians perceive their performance of sub-processes of diagnosis, for example information seeking and information integration. This study analyzed the performance data of an experiment of diagnosing an accident in a simulated nuclear power plant. The objective performance was measured by eight indicators and the perceived performance was measured by three indicators. Difference relations and correlations between these indictors were explored. Results showed that on one hand there were systematic deviations between perceived and objective performance, on the other hand the perceptions did have some validity. Perceptions of information seeking manifested under-confidence while perceptions of information integration and the overall diagnosis manifested over-confidence. The authors argue that these two biases were mutually complementary and facilitating rather than contradictory. The findings could be used to help diagnosis-related training, operation and decision making.

安全级DCS是核电厂的安全重要部分,对设备的安全性及可靠性要求较高.火灾作为影响其安全可靠运行的内部事件,它的发生将会导致DCS设备故障和误操作.为预防火灾发生及限制火灾后果,使火灾产生的影响降到最低,对安全级DCS机柜提前进行火灾仿真,预测机柜内的火灾薄弱部位显得尤为重要.本文主要通过建立的安全级DCS机柜火灾仿真流程,分析机柜可燃物,对机柜的火灾过程数据进行仿真演示,模拟机柜内的烟雾运动、火焰蔓延等动态发展情况,同时对机柜火灾模拟数据进行分析,提出机柜优化设计改进方案,来保证机柜的高可靠性.

对核电安全级数字化控制系统(SDCS)机柜结构进行详细设计,采用有限元分析中的响应谱分析法,对该设备的抗震特性进行校核.加工出设备样机进行抗震性能鉴定试验,对地震作用下机柜的结构响应特性与抗震性能进行分析.研究结果表明:该核电仪控机柜首阶模态频率为15.257 Hz,其主要振型为机柜框架整体沿横向的偏摆运动,机柜的自然频率远离地震幅值放大区,具有一定的安全裕度.响应谱分析结果表明:在机柜的首阶模态振型与配重区域共同作用下,机柜最大应力位于机柜右前立柱与底框的焊接区域,最大Mises应力为158 MPa,小于机柜材料的屈服极限,因此在地震作用下该型机柜具有较好的抗震能力.地震试验分析结果表明:地震台面的振动信号在逐渐传递至机柜的过程中经过一定程度的放大.在纵向方向上,机柜重心处的振动加速度幅值最大.在横向方向上,振动信号放大最为明显,振动幅值随着机柜高度逐渐变大,使得在机柜柜顶区域,地震信号放大效果最为显著.抑制机柜的横向运动是改善结构抗震性能的关键.设计的核电仪控系统抗震机柜顺利地通过核级设备抗震试验,所提出的设计、分析、试验和结果为核电仪控机柜的设计提供参考依据.

后备盘(BUP)主要作为核电厂主控制室数字化技术失效后的备用手段,用于安全停堆并将反应堆维持在冷停堆水平以及事故工况下处理.后备盘实现报警、显示和控制三类功能,其安全、可靠性对于保障反应堆安全停堆十分重要.开展对核电厂后备盘的辐射散热以及自然对流的热分析模拟,定量地对辐射换热以及自然对流在后备盘中所起的作用进行分析说明,掌握后备盘散热的机理.研究结果表明,通过仿真模拟得到的后备盘内部的最高温度在为60℃,满足电源模块最高运行温度70℃的要求;后备盘散热过程中辐射换热过程占据较大的比例,辐射换热与自然对流的比例大概为6∶1,空气自然对流对机柜本身造成的温升可以忽略;真实后备盘内部的结构件与线缆对自然循环散热以及辐射换热所造成的影响可以忽略.该研究结果与经验可以为复杂工况下的核动力仪控设备的散热分析提供参考.

The translation-based virtual DCS based on Simulink can realize the function of virtualizing the physical DCS. This paper presents a method to virtualize physical DCS by using Simulink to realize the functions of running, freezing, acceleration and deceleration, setting and acquiring variable values, malfunction simulation, snapping and loading initial conditions, etc. Virtual DCS realizes the configuration translation by translating the configuration files of the physical DCS platform to Simulink platform, generating codes by using the configuration, and compiling the codes into algorithm files. The virtual DCS is combined with process model software to form a closed-loop, which simulates the level control system of the steam generator of a megawatt pressurized water reactor nuclear power plant for verification. Effective results have been achieved, which proves that the translation virtual DCS can meet the simulation effect of the simulator.

The algorithm for the 1E system of NPPs is generally developed by a graph making tool at the engineering station. After the executable file is generated by the compiler and downloaded to the platform software, the credibility of the executable algorithm depends on the credibility of the generated programming code. Therefore, its security requirements put high demands on the compiler. The formal method has been developed rapidly in response to the problem of trusted compilation in recent years. This paper studies the main methodology and key technological components for designing and implementing the trusted compilers, meanwhile emphasize its industrial application based on existing research. The application is optimized, and a new composite compilation architecture is proposed, which reduces the difficulty of proof work and enhances the flexibility of the compiler’s later phase. Finally, several compiler optimization procedures for the security level software NASPIC are studied, and the algorithm compilation is enhanced, as well as the trusted performance of the device.

In nuclear power plant embedded software control area, graphical control algorithms are described by Lustre program and designed with graphical editors of engineering station. After they are translated into C programs through a code generator, then the C programs are downloaded to the embedded platform software of NASPIC. The correctness of the code generator will directly determine the credibility and safety of NASPIC. Therefore, it’s important to ensure the correctness of the code generator translation process. Formally verified the correctness of a code generator, which has been studied for many years and becomes a most effective approach to develop a trusted code generator. This article is based on the requirements of nuclear safety-level I&C (Instrumentation & Control) system and mainly presents the development of a formally verified code generator front-end. The front-end translates Lustre source program into S_Lustre (a sequential intermediate language). And it is programmed and proved in Coq (Auxiliary Theorem Prover). During the development of the front-end, two key technical challenges have been resolved. The first is to ensure every id which appeared in the Lustre program has been defined. The second is to implement the casualty analysis and determine the evaluation order of user-defined types and equations based on the dependencies.