摘要
目前,核能装备等安全关键系统中软件的作用越来越重要,对系统的安全稳定运行具有至关重要的影响。安全关键软件规模的增长和复杂度的增加给设计和开发高可信的软件带来了新的挑战,亟需新的软件开发和验证方法与模式。针对此需求,本文围绕核能装备安全控制代码自动生成软件研究面临的三大关键科学问题,分别开展一个基础理论、七大关键技术及一套原型系统的研究。通过核能安全控制代码自动生成软件总体设计集成与评估、核能安全控制与交互系统软件建模技术、核能安全控制系统模型分析与验证技术、核能安全控制系统可信软件代码自动生成技术等方面的研究,突破核能装备安全控制代码自动生成软件在建模、代码生成和测试验证面临的系统性技术瓶颈,建立起新的安全关键软件开发和验证方法与模式。通过可信安全控制代码自动生成软件工程化应用与认证技术研究,构建一个核能装备安全控制代码自动生成的原型系统,并在核能、汽车等领域对研究成果进行验证。通过上述研究实现以下5个方面创新:一是形式化方法与模型驱动开发融合理论,用确定的数学理论保证模型的高可信;二是状态机扩展同步数据流语言形式化定义方法,建立适用于核能、航空、汽车等场景的软件建模方法;三是基于交互式定理证明的可信代码生成器构造方法,形成经过形式化验证的可信代码生成器;四是数据驱动的测试用例智能生成方法,实现测试验证的自动化;五是一套面向核能装备控制软件的一体化研发平台,构建完整的开发和验证工具链。本文旨在以形式化和模型驱动方法为基础,对安全关键软件的建模、模型验证、代码生成、测试验证等方面进行系统性研究,以形成高可信的安全关键软件开发和验证新方法。研究成果对核能等领域安全关键软件开发相关工业软件的科学研究、技术研发、产业发展等具有十分重要的理论意义和实际应用价值。
The role of software is crucial for the stable operation of safety-critical systems such as nuclear equipment.In the face of the advance-ment and complexity of safety-critical software,new challenges are encountered in the design and development of highly reliable software,and new methods and paradigms for software development and verification are urgently needed.Both formal methods and model-driven techniques have gained increasing attention in this field.In response to this demand,combined with the latest technological trends,this paper focuses on three key scientific problems and explores one basic theory and seven key technologies.Additionally,a prototype software platform is developed.Aim-ing to overcome the technical bottleneck faced by automatic code-generation software for nuclear equipment in modelling,code generation,test-ing,and verification,we perform the following tasks:overall design and evaluation of automatic code-generation software for nuclear safety con-trol systems,software modelling technology for nuclear safety control and human-machine interactive systems,model analysis and verification technology for safety control systems,and automatic code-generation technology for verified software for safety control systems.Based on this re-search,we establish a new safety-critical software development and verification method and paradigm.Moreover,we construct a prototype auto-matic code-generation system for safety control in nuclear equipment,applying verified software and safety-certification technology.With regard to the overall design and evaluation of the software platform,we perform requirements analysis considering specific application scenarios in vari-ous fields and construct domain models.We design the architecture of the software platform and examine the key platform technologies and meth-ods to support module development,functional safety,and compliance with standards.It is necessary to solve the scientific problem of the formal method and model-driven fusion theory and develop a novel technology for safety control software code based on the architecture design of a model-based development environment.In software modelling,it is essential to accurately describe the requirements of the target system in the nuclear domain,characterize the control,interaction,and coordination of the target system,realize accurate modelling of the nuclear domain mod-el,and provide a basis for the analysis and verification of the relevant safety properties of the subsequent model,simulation,and code generation.These can be achieved by solving the scientific problems of the formal semantic theory of nuclear control and the human-interaction model and developing two key technologies:enhanced synchronous data flow modelling technology with safety embedded state machines and graphical hu-man-computer interaction configuration technology for nuclear control systems.In terms of model analysis and test verification,the correctness verification of the safety control system model based on formal and simulation methods should be completed.To achieve this,following key tech-nologies should be developed:model correctness checking technology for safety control systems,intelligent generation and accurate testing tech-nology for high coverage test cases,a general high-reliability virtual simulation driver,and automatic execution technology.In terms of code gen-eration,a highly verified code generator should be developed based on formal verification of transformation from the nuclear power control and interaction system modelling language to a domain-specific safe subset of the C language.It is necessary to solve the scientific problem of the re-liable construction theory and synchronous data flow model code generator of control systems extended by safety state machines and develop the key technology for formal verification of synchronous data flow language verified code generators based on theorem proof.The main innovations introduced in this study are as follows:First,we present a new method for developing nuclear safety control software based on the integration of formal methods with model-driven development.This approach guarantees both the reliability of the software and the efficiency of its develop-ment.We provide a theoretical basis for the abstract transformation from software code to theorems,and also study,deploy,and schedule the con-struction of the tool chain around formal verification.Second,we extend the state-machine schema to construct a new language(based on the Lustre language)conforming to the synchronous data-flow theory.A complete and accurate description of complex control logic in safety-critical domains such as nuclear power equipment is provided.Third,we propose a verified code generator based on interactive theorem proving and use it to explore and solve the problem of generating high-reliability safety control code.Fourth,we propose a data-driven and intelligent test-case generation method based on machine learning for exploring the correlation between abstract models and software codes.Finally,we describe an integrated development platform for nuclear safety control software that meets high-level quality and safety requirements.It includes model-based design,simulation,verification,code generation,and other functions,providing one-stop solutions for software development in safety-critical areas.The goal of our research is to offer a new and highly reliable method for developing and verifying safety-critical software.Our results have considerable theoretical and practical implications for scientific research and development of industrial software in domains such as nuclear equip-ment.
作者
刘明星
马权
吴鹏
杨斐
侯荣彬
王俊峰
黄滟鸿
吴延群
LIU Mingxing;MA Quan;WU Peng;YANG Fei;HOU Rongbin;WANG Junfeng;HUANG Yanhong;WU Yanqun(College of Computer Sci.,Sichuan Univ.,Chengdu 610065,China;Sci.and Technol.Reactor System Design Technol.Lab.,Nuclear Power Inst.of China,Chengdu 610213,China;School of Software Eng.,East China Normal Univ.,Shanghai 200241,China)
出处
《工程科学与技术》
EI
CAS
CSCD
北大核心
2024年第2期1-16,共16页
Advanced Engineering Sciences
基金
国家重点研发计划项目(2022YFB3305200)
四川省重大科技专项(2022ZDZX0008)。
关键词
核能装备
代码生成
形式化
模型驱动
nuclear equipment
code generation
formal
model-driven
