发表机构
Université Grenoble Alpes - CNRS - Grenoble INP - Verimag; Framatome GmbH（格勒诺布尔阿尔卑斯大学-法国国家科学研究中心-格勒诺布尔理工学院-Verimag; Framatome有限公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对TELEPERM XS核安全I&C平台的编译验证需求，研究引入CompCert认证编译器，借助形式化方法解决特定代码模式的性能问题，同时缩小可信计算基以强化系统安全论证。
AI 中文摘要
民用核电厂（NPP）中的大型安全仪表与控制（I&C）系统主要是安全停堆系统（反应堆保护）或限制与控制系统。Framatome成熟的TELEPERM XS（TXS Core）产品系列是覆盖所有这类应用的数字化I&C系统平台。我们阐述了验证在软件生产工具链不同阶段的作用，聚焦于形式化编译流程，并讨论了CompCert认证编译器对该产品安全论证的贡献。对该编译器生成的目标代码的审查发现，在某类简单但反复出现的生成代码模式中，运行时性能欠佳。我们解释了形式化方法如何让我们在编译器中解决这一问题，同时缩小其可信计算基（TCB），从而强化而非仅仅维持安全论证。
英文摘要
The large safety instrumentation & control (I&C) systems in civil nuclear power plants (NPPs) are mainly safe-shutdown systems (reactor protection) or limitation and control systems. Framatome's established TELEPERM XS (TXS Core) product family is a digital I&C system platform to cover all these applications. We illustrate the role of verification in the different stages of the software production toolchain, focus on the formal compilation process, and discuss the contribution of the CompCert certified compiler to the safety case of the product. Scrutinizing the object code produced by this compiler has exhibited suboptimal run-time performance in a certain simple but recurring generated code pattern. We explain how formal methods allow us to address this issue in the compiler while simultaneously reducing its trusted computing base (TCB), thereby strengthening the safety case rather than merely preserving it.
CommentsIn Proceedings FROM 2026, arXiv:2609.30324
Journal refEPTCS 452, 2026, pp. 92-103
