核 能 装 备 安 全 控 制 代 码 自 动 生 成 软 件 研 发 与应 用 的 构 想 与 成 果 展 望

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.