Formal Verification of a Nuclear Plant Thermal Dispatch Operation Using System Decomposition

This paper discusses methods to prove the safety of critical cyber-physical systems. Critical infrastructure, such as nuclear power plants, are prone to vulnerabilities due to the integration of industrial internet-of-things technologies. Automation and computation introduces greater complexity into these systems. Thus, traditional safety analysis methods, including probabilistic risk assessment and system theoretic process analysis, can be limited in their scope of analysis, specifically in addressing software vulnerabilities and the cyber-physical interface. To address these limitations, we propose an approach to safety analysis by integrating multiple formal verification methods within the context of hybrid systems. This approach employs a combination of reachability analysis and theorem proving, specifically using differential dynamic logic (dℒ), to model and verify the safety of a nuclear plant’s thermal dispatch operation. By decomposing the system into individual components, our method reduces computational complexity and enhances the verification process, ensuring the resiliency of critical infrastructure against potential hazards. This integrated approach offers a comprehensive framework for the safety and security of complex, cyber-physical systems.