一种面向核能自动化控制系统的高安全性PLC编译验证方法

本发明公开了一种面向核能自动化控制系统的高安全性PLC编译验证方法，涉及软件工程与核能控制技术领域，包括以下步骤：首先设计适用于核能控制系统的PLC语言子集ST‑light；其次基于大步语义学构建ST‑light的语义模型；紧接着设计ST‑light到Clight的可信编译算法；包括：进行类型检查，确保变量类型匹配；生成Clight代码；采用CompCert可信编译链将Clight转换为目标代码；最后使用定理证明技术对设计的可信编译算法的语义一致性进行证明；本发明提供的方法，避免了编译错误导致的系统故障，从而提高核能设施的运行可靠性。