Physical Address
304 North Cardinal St.
Dorchester Center, MA 02124
IEC TR 61838:2009 — 核电厂仪控系统形式化方法应用指南
核安全系统形式规约与验证技术指导手册
关键要点
IEC TR 61838:2009 提供了在核电厂安全关键仪控系统的规约、设计和验证中应用基于数学的形式化方法的全面指导，帮助实现安全功能所需的最高系统完整性等级。
IEC TR 61838:2009 提供了在核电厂安全关键仪控系统的规约、设计和验证中应用基于数学的形式化方法的全面指导，帮助实现安全功能所需的最高系统完整性等级。
1. 标准范围与目的
IEC TR 61838:2009 是一份技术报告，为核电厂仪控系统开发中使用形式化方法提供指导。形式化方法是基于数学的技术，用于软件和硬件系统的规约、开发和验证。与传统测试只能证明错误的存在而不能证明其不存在不同，形式化方法能够提供严格的证明，确认系统在所有可能的运行条件下满足其指定的属性。该标准涵盖完整的开发生命周期，包括需求形式化、使用形式语言进行系统规约、基于精化的设计和通过定理证明与模型检测进行的形式验证。它旨在补充IEC 61513的系统级要求和IEC 60880的软件要求。
适用性说明
IEC TR 61838 是一份提供指导而非要求的技术报告。它描述了形式化方法应用的推荐实践，但未强制要求特定的形式语言、工具或验证技术。适当的应用水平取决于仪控系统的安全分级。
IEC TR 61838 是一份提供指导而非要求的技术报告。它描述了形式化方法应用的推荐实践，但未强制要求特定的形式语言、工具或验证技术。适当的应用水平取决于仪控系统的安全分级。
2. 形式化方法分类与应用
该标准将形式化方法分为几个系列，每个系列适用于核电厂仪控系统开发的不同方面。方法的选择取决于所针对的系统特征、开发阶段和所需的安全完整性等级。
| 形式化方法类型 | 数学基础 | 主要应用 | 典型工具 | 适用场景 |
|---|---|---|---|---|
| 基于模型 (Z, B, VDM) | 集合论、谓词逻辑 | 系统规约、数据建模 | Atelier B, Rodin, Z/Eves | 高层系统需求和架构 |
| 基于状态 (SCADE, Statecharts) | 有限状态机、数据流 | 控制逻辑和时序 | SCADE Suite, Statemate | 反应式控制系统 |
| 时序逻辑 (CTL, LTL) | 含时序算子的模态逻辑 | 属性规约、验证 | NuSMV, SPIN, UPPAAL | 并发和实时特性 |
| 过程代数 (CSP, CCS) | 通信过程代数 | 并发建模、协议验证 | FDR, CADP, mCRL2 | 通信协议、联锁逻辑 |
| 定理证明 (HOL, Coq) | 高阶逻辑、类型论 | 无限状态验证、通用证明 | Isabelle/HOL, Coq, PVS | 安全论证形式化 |
| 模型检测 | 自动机理论、CTL/LTL | 自动属性验证 | NuSMV, SPIN, UPPAAL | 设计的有限状态验证 |
2.1 形式化开发过程
该标准描述了与整个仪控系统生命周期集成的结构化形式化开发过程。该过程始于将以自然语言表达的系统需求形式化为数学上精确的规约。然后通过逐步精化将形式规约转化为可实施的设计，在每个精化步骤中生成证明义务以证明正确性。精化过程通过构造保证正确性——如果初始规约是正确的并且每个精化步骤都经过验证，则最终实现保证满足原始需求。标准强调形式化方法应有选择地应用，重点关注安全关键功能，在这些功能上额外的严谨性相对于应用成本提供最大的收益。
2.2 形式化方法的验证与确认
形式验证技术作为传统测试和评审的补充方法。模型检测穷尽地探索有限状态模型的所有可达状态，以验证指定的属性是否成立。定理证明使用逻辑推导来证明可能具有无限状态空间的系统的正确性属性。标准建议组合应用多种验证技术以达到所需的置信水平。对于被分类为安全关键的系统（根据IEC 61226的A类），形式验证应应用于所有安全功能，而对于较低安全等级的系统，选择性地对最复杂或最危险的功能应用就足够了。
工程最佳实践
形式化方法在核电仪控中最有效的应用是联锁和保护逻辑的规约和验证。这些系统通常足够复杂，值得进行形式分析，同时状态空间有限，对于模型检测工具是可处理的。成功应用形式化方法的公司报告，与传统评审技术相比，可在需求层面多发现2-5倍的错误。
形式化方法在核电仪控中最有效的应用是联锁和保护逻辑的规约和验证。这些系统通常足够复杂，值得进行形式分析，同时状态空间有限，对于模型检测工具是可处理的。成功应用形式化方法的公司报告，与传统评审技术相比，可在需求层面多发现2-5倍的错误。
3. 工具支持与实施
该标准为核安全应用中选择和鉴定形式化方法工具提供指导。用于安全关键开发的工具本身必须经过适当完整性等级的鉴定，标准涉及了对工具输出所需置信度的考量。
| 实施方面 | 建议 | 挑战 | 缓解策略 |
|---|---|---|---|
| 工具鉴定 | 使用在核领域有良好记录的工具 | 合格工具可用性有限 | 针对参考案例进行工具验证 |
| 人员能力 | 形式记法和工具的专门培训 | 工程师学习曲线陡峭 | 分阶段采用、专家指导 |
| 与现有流程集成 | 形式化方法作为现有V&V的补充 | 流程重叠和冗余 | 将形式活动清晰映射到V&V任务 |
| 可扩展性 | 将系统分解为可验证的模块 | 模型检测中的状态空间爆炸 | 抽象技术、组合验证 |
| 维护 | 系统变更时更新形式模型 | 模型与实际实现偏离 | 将模型与代码关联的配置管理 |
3.1 与软件生命周期过程的集成
该标准描述了形式化方法如何与IEC 60880为核安全软件定义的软件生命周期过程集成。形式规约活动在需求分析阶段进行，生成可以数学分析其一致性、完备性和无歧义性的形式需求文档。在设计阶段，形式精化将规约转化为详细设计表示。可以使用经过鉴定的代码生成器从经过验证的形式模型自动生成代码，消除了手动编码和相关编码错误。验证活动贯穿整个生命周期，形式证明补充传统测试。标准建议将形式模型作为生命周期内持续更新的活动制品，随设计变更进行更新并用于变更期间的回归验证。
3.2 经济性考虑
虽然形式化方法需要在培训和工具方面投入大量前期成本，但标准指出经济效益通过减少返工成本、更早发现需求错误以及为监管审批提供更强的安全证据来实现。标准引用的研究表明，在形式规约阶段发现的需求错误，其纠正成本比在系统测试阶段发现的同样错误低10-50倍。对于核安全关键仪控系统，在生命周期后期发现单个错误的成本可能极高，因此对于A类和B类功能，形式化方法应用的投资回报率通常是正的。
关键考虑
采用形式化方法时最大的风险是形式模型与实际实施系统之间的脱节。如果实现变更时形式模型没有更新，验证结果就失去意义。工程组织必须建立严格的配置管理程序，将形式模型与源代码和设计文档一起视为主要开发制品。
采用形式化方法时最大的风险是形式模型与实际实施系统之间的脱节。如果实现变更时形式模型没有更新，验证结果就失去意义。工程组织必须建立严格的配置管理程序，将形式模型与源代码和设计文档一起视为主要开发制品。
4. 常见问题解答
问题1：形式化方法能否保证无错误的软件？
形式化方法可以证明软件正确实现了其形式规约，但不能保证形式规约正确捕获了所有利益相关者的需求。此外，形式验证应用于抽象模型，不一定适用于编译后的可执行代码。编译器正确性、硬件行为和操作系统服务需要单独保证。形式化方法显著降低了系统故障的可能性，但不能完全消除。
问题2：哪些核仪控功能从形式化方法中获益最多？
安全关键逻辑功能（根据IEC 61226的A类分类）获益最大，特别是反应堆保护系统、工程安全设施驱动系统和联锁逻辑。这些功能具有可以形式规约的明确定义的安全属性、状态空间足够有限以进行验证，以及极高的故障后果，证明了额外严谨性和成本的合理性。
问题3：IEC TR 61838 与 IEC 60880 的关系是什么？
IEC 60880 规定了核安全系统的软件要求，并提到形式化方法是最高软件完整性等级的推荐技术。IEC TR 61838 提供了如何在IEC 60880 软件生命周期框架内选择、应用和集成形式化方法的详细指导。两份文件是互补的——IEC 60880 说明”必须做什么”，而IEC TR 61838 解释”如何用形式化方法来做”。
问题4：采用形式化方法的主要挑战是什么？
主要挑战包括：（1）对于通常更熟悉传统编码和测试的工程师来说，学习曲线陡峭；（2）经鉴定可用于核安全应用的形式化方法工具可用性有限；（3）形式验证扩展到大型系统的困难；（4）在系统40-60年运行寿命中维护形式模型的挑战。这些挑战可以通过从专注于明确定义的子系统的试点项目开始的阶段性采用来解决。
