核能装备安全控制代码自动生成软件研发与应用的构想与成果展望

摘要

目前，核能装备等安全关键系统中软件的作用越来越重要，对系统的安全稳定运行具有至关重要的影响。安全关键软件规模的增长和复杂度的增加给设计和开发高可信的软件带来了新的挑战，亟需新的软件开发和验证方法与模式。针对此需求，本文围绕核能装备安全控制代码自动生成软件研究面临的三大关键科学问题，分别开展一个基础理论、七大关键技术及一套原型系统的研究。通过核能安全控制代码自动生成软件总体设计集成与评估、核能安全控制与交互系统软件建模技术、核能安全控制系统模型分析与验证技术、核能安全控制系统可信软件代码自动生成技术等方面的研究，突破核能装备安全控制代码自动生成软件在建模、代码生成和测试验证面临的系统性技术瓶颈，建立起新的安全关键软件开发和验证方法与模式。通过可信安全控制代码自动生成软件工程化应用与认证技术研究，构建一个核能装备安全控制代码自动生成的原型系统，并在核能、汽车等领域对研究成果进行验证。通过上述研究实现以下5个方面创新：一是形式化方法与模型驱动开发融合理论，用确定的数学理论保证模型的高可信；二是状态机扩展同步数据流语言形式化定义方法，建立适用于核能、航空、汽车等场景的软件建模方法；三是基于交互式定理证明的可信代码生成器构造方法，形成经过形式化验证的可信代码生成器；四是数据驱动的测试用例智能生成方法，实现测试验证的自动化；五是一套面向核能装备控制软件的一体化研发平台，构建完整的开发和验证工具链。本文旨在以形式化和模型驱动方法为基础，对安全关键软件的建模、模型验证、代码生成、测试验证等方面进行系统性研究，以形成高可信的安全关键软件开发和验证新方法。研究成果对核能等领域安全关键软件开发相关工业软件的科学研究、技术研发、产业发展等具有十分重要的理论意义和实际应用价值。

关键词

核能装备 / 代码生成 / 形式化 / 模型驱动