刘明星1,2，马权2*，吴鹏1，杨斐2，侯荣彬2，王俊峰1，黄滟鸿3，吴延群2

（1.四川大学计算机学院，四川成都 610065；2.中国核动力研究设计院核反应堆系统设计技术重点实验室，四川成 610213；3.华东师范大学 软件工程学院）

创新点

论文包括以下5个方面创新：一是，形式化方法与模型驱动开发融合理论，用确定的数学理论来保证模型的高可信；二是，状态机扩展同步数据流语言形式化定义方法，建立适用于核能、航空、汽车等场景的软件建模方法；三是，基于交互式定理证明的可信代码生成器构造方法，形成经过形式化验证的可信代码生成器；四是，数据驱动的测试用例智能生成方法，实现测试验证的自动化；五是，一套面向核能装备控制软件的一体化研发平台，构建完整的开发和验证工具链。

选题依据

核能装备等安全关键系统中软件的作用越来越重要，对系统的安全稳定运行具有至关重要的影响。安全关键软件规模的增长和复杂度的增加给设计和开发高可信的软件带来了新的挑战，亟需新的软件开发和验证方法与模式。本研究旨在以形式化和模型驱动方法为基础，对安全关键软件的建模、模型验证、代码生成、测试验证等方面进行系统性研究，通过核能安全控制代码自动生成软件总体设计集成与评估、核能安全控制与交互系统软件建模技术、核能安全控制系统模型分析与验证技术、核能安全控制系统可信软件代码自动生成技术等方面的研究，突破核能装备安全控制代码自动生成软件在建模、代码生成和测试验证面临的系统性技术瓶颈，构建起新的安全关键软件开发和验证方法与模式。

研究方案或路线

研究内容与数据

（1）核能安全控制代码自动生成软件总体设计集成与评估研究；

基于模型的开发与基于模型的系统工程的概念，制定针对核能装备控制代码开发的应用方案；研究形式化方法的原理、方法、技术、应用。研究各个安全关键领域对整个软件平台的功能需求、非功能需求及安全要求；构建各领域通用的领域模型；围绕建模、代码生成、测试、仿真、验证模块开展软件架构设计。

（2）核能安全控制与交互系统软件建模技术研究；

研究核能控制与交互系统建模语言的语法定义与形式化语义解释，利用严密和准确的数学符号保证模型的准确性；定义建模语言的语义状态集用于描述模型需要展示的信息；给出建模语言中各类语法算子的迁移规则，刻画模型的动态行为。

（3）核能安全控制系统模型分析与验证技术研究；

研究安全级控制系统静态验证与动态验证相结合的组合分析验证方法，结合控制流模型安全属性约束与Lustre数据流语义模型，实现对安全攸关控制系统的可靠性、安全性进行动静结合的分析证明；研究基于语义执行的模型动态仿真方法，结合内存周期快照的模型数据监测与调试，提出安全级控制与交互系统动态仿真框架；研究基于事件驱动的测试用例自动执行方法，结合测试用例调度策略以及高效数据存储策略，实现安全级控制与交互系统动虚拟仿真驱动及测试用例自动执行。

（4）核能安全控制系统可信软件代码自动生成技术研究；

研究状态机扩展的控制系统同步数据流模型的特性，精确定义其静态与动态语义；在此基础上，全面分析研究同步状态机核心特性以及重要的扩展特性的代码生成和优化策略与算法；并深入研究代码生成和优化算法的正确性验证方法，制定形式化验证目标和验证方案。研究在交互式定理证明辅助工具中完成翻译过程、分析或翻译确认过程的构造及其正确性证明的核心技术问题。

（5）可信安全控制代码自动生成软件工程化应用与认证研究。

针对不同的应用领域，对平台软件进行工程化开发，形成工程化平台。在核能领域，依托中国工程试验堆，展开需求分析、平台搭建、应用代码开发，完成平台软件在工程试验堆的应用验证。依托华龙一号核电站，通过开展需求分析、保护系统典型功能识别、虚拟仿真验证环境搭建、应用代码开发等完成平台软件在华龙一号的应用验证。依托智能汽车，展开需求分析、平台搭建、应用代码开发，建立工程验证环境，完成平台软件在智能汽车的应用验证。

主要结论

通过研究模型驱动和形式化方法融合为创新理论和方法，攻克核能装备安全控制代码自动生成软件在建模、代码生成和测试验证面临的系统性关键技术，构建起新的安全关键软件开发和验证方法与模式，开发形成一套面向核能装备控制软件的一体化开发和验证平台。研究成果可解决核能领域关键工业软件长期面临“卡脖子”问题，支撑核能等安全关键领域软件开发和验证，提升安全关键软件的开发质量和效率。

作者简介

通信作者

马权，博士，研究员级高级工程师，中国核动力院仪控中心副主任，四川大学客座研究员/博士导师。主要研究方向反应堆控制。科技部国家重点研发计划“核能装备安全控制代码自动生成软件研发与应用”项目负责人/首席科学家。主持完成我国首套多用途数字化核安全级DCS系统“龙鳞”，被叶奇蓁院士等专家鉴定为“部分关键技术国际领先”。相关成果已应用到华龙一号核电、中国工程实验堆等多个国家重大工程中，合同总金额超30亿，社会经济效益显著。主持研制的“龙鳞系统”随国之重器“华龙一号”搭载四川彩车，成功亮相在国庆70周年阅兵仪式上。获省部级科技进步二等奖3项（排名2、2、8）、三等奖3项、银奖1项。授权发明专利29项、发表学术论文24篇。入选国家高端人才、四川省高端人才、四川省学术和技术带头人，荣获中国青年五四奖章，获四川省杰出青年科技人才基金支持。

团队简介

中国核动力研究设计院核安全级DCS研发团队长期围绕核反应堆关键仪控系统和设备自主化和国产化开展研究工作，致力于提升核反应堆关键仪控系统的数字化、智能化水平，推动我国核反应堆关键仪控系统的技术研发与设备保障。团队有正高级工程师15人，博士12人，在相关领域发表论文100余篇，授权专利130余项，获15项省部级以上科技奖励，承担了科技部、科工局、四川省科技厅等50余项国家级、省部级重点研究项目。团队自主研发的核安全级DCS“龙鳞系统”打破了国外垄断，实现了我国核电站“中枢神经”系统的国产化，在中国工程试验堆、华龙一号核电站等多个国家重大工程中实现批量化应用，直接经济效益超30亿元，有力保障了我国多项核设施的建设和安全运行。

引用格式

Liu Mingxing,Ma Quan,Wu Peng,et al.Automatic code-generation software for nuclear safety control systems:Research framework and anticipated results[J].Advanced Engineering Sciences,2024,56(2):1–16.[刘明星,马权,吴鹏,等.核能装备安全控制代码自动生成软件研发与应用的构想与成果展望[J].工程科学与技术,2024,56(2):1–16.]

扫码阅读全文

《工程科学与技术》是由教育部主管、四川大学主办的工程科学综合性学术期刊，主编谢和平院士，拥有包括17位中外院士及8位国际专家的高水平国际化的编委团队。期刊以“建设具有国际影响力的一流科技期刊”为目标定位，报道工程科学领域研究、开发及应用的有创造性的学术论文。期刊发文覆盖土木、水利、计算机、机械、环境、信息、交通、电气、网安、控制、地质、材料、化工、矿业等学科领域。开设的“聚焦国家重点研发计划”“碳中和与绿色能源”“川藏铁路工程与环境”“新型电力系统”等特色栏目，受到国内外读者的广泛关注，产生了较大的学术及社会影响力。期刊被《EI》《Scopus》《EBSCO数据库》《中国科学引文数据库（CSCD）核心版》《中国科技论文与引文数据库（CSTPCD）（中国科技核心期刊）》《中文核心期刊要目总览》等国内外重要数据库收录。期刊被评为中国中文权威学术期刊（A+等级），入选“中国精品科技期刊”“天府期刊卓越行动计划-卓越期刊”。期刊位于《世界影响力指数报告》Q2区，纳入了四川大学认定的高质量科技期刊范围。

｜欢迎关注