An advanced solution for nuclear safety I&C software: Deep integration of model-driven development and formal methods

Instrumentation and control (I&C) systems constitute the central nervous system of a nuclear power plant. In digital I&C systems, software is the core carrier of functionality and may be regarded as the “cognition” of the plant. With the rapid growth in both the complexity and scale of software functions, software reliability—especially for safety-class software—has become a critical challenge. Formal methods offer a promising solution to this challenge; however, in the nuclear domain, their application remains fragmented and exploratory, lacking a systematic methodology and integrated framework. In this paper, we propose a deeply integrated framework that combines model-driven development with formal methods across the entire software lifecycle. The framework addresses, in a formal and unified manner: (1) the precision of software requirements and design specifications, (2) behavioral consistency between software design and implementation, and (3) conformance of software design to formalized requirements. The framework integrates formal requirements specification, synchronous dataflow-based design modeling, formal verification, and semantics-preserving code generation into a traceable workflow. It is implemented in the LoongMeta toolchain and evaluated using representative functions from the Hualong One (HPR1000) reactor protection system and the Linglong One (ACP100) power control system. The evaluation achieved an automatic code generation rate of 90%, 100% behavioral consistency between the design models and generated C code, and an approximately 30% improvement in overall engineering efficiency. Overall, these results show that the deep integration of model-driven development and formal methods provides a practical, traceable, and quantitatively assessable approach to quality assurance for safety-critical nuclear I&C software.