基于微分动态逻辑的数字化反应堆控制系统建模与验证方法

核电数字化仪系统既涉及反应堆随时间变化的物理动态演化过程，又涉及计算机的离散控制过程，属于典型的实时混成系统。微分动态逻辑是近年在混成系统验证领域的新方法。提出以微分动态逻辑为基础的构建反应堆控制系统安全验证模型方法，验证反应堆控制系统中离散化的逻辑控制与反应堆连续性的物理连续变化过程之间的相互作用能否保证反应堆安全需求，从而提高数字化反应堆控制系统设计的安全性。

Study on modeling and verification methods of digital reactor control system based on differential dynamic logic

Digital reactor control system is a typical real-time hybrid system involving the physical dynamic evolution process of reactor against time and the discrete control process of computer. Differential dynamic logic is a new theory for hybrid system verification. A new method to construct safety verification model of digital reactor control system based on differential dynamic logic was put forward, so as to verify whether the interaction between discrete logic control in reactor control system and the physical continuous change process of reactor continuity can guarantee the safety requirement of reactor. It improves the safety properties of design on digital reactor control system.