第27卷  第11期2020年11月仪器仪表用户INSTRUMENTATION
Vol.272020  No.11
核安全级DCS系统模型驱动可信代码自动生成方法
兰 林1,2，马 权1，侯荣彬1，李 勇1，杨 斌1，荣健兵1，吴延1
（1.中国核动力研究设计院 核反应堆系统设计技术重点实验室，成都 610213；
2.哈尔滨工程大学，哈尔滨 150000）
摘    要：
为了提高核安全级DCS 系统控制算法的设计效率和打破关键建模软件完全依赖国外进口的局面，基于对图形化建模技术和形式化验证技术的研究，提出了一种集图形化建模和可信代码自动生成于一体的核安全级DCS 系统控制算法的开发方法，将极大地提高核安全级DCS 系统控制算法开发效率。主要介绍了图形化建模软件、XML 文件数据提取方法和可信代码生成软件的设计，将这些软件集成后，为核安全级DCS 系统控制算法开发，提供了一套由模型驱动代码自动生成的解决方案。关键词：可信代码自动生成；XML ；形式化验证
中图分类号：TP273                文献标志码：A
The Graphical Algorithm Model Drives the Generation of Trusted Code in
Safety Level DCS
Lan Lin 1,2，Ma Quan 1，Hou Rongbin 1，Li Yong 1，Yang Bin 1，Rong Jianbing 1，Wu Yanqun 1
（1. Science and Technology on Reactor System Design Technology Laboratory
Nuclear Power Institute of China, Chengdu, 610213, China；2. Harbin Engineering University, Harbin, 150000,China）
Abstract： In order to improve the level of the nuclear security replication system control algorithm design efficiency and break entirely dependent on foreign import situation, based on the graphical modeling and formal verification technology research, implements a set of graphical modeling equipment, modeling variables, modeling algorithm, XML file information extraction and trusted code automatically generated in the integration of nuclear safety level of DCS system model driven trusted code automat-ically generated method, greatly improved the nuclear all control engineer control algorithm development efficiency. It mainly introduces the design and implementation of graphical mod
eling software, XML file data extraction software and trusted code generation software.
Key words：trusted code generation；XML；formal verification
0  引言
核安全级仪控DCS 系统（Nuclear Advanced Safety Platform Instrument Control System，简称NASPIC）对于核电厂的安全、稳定运行具有重要的作用，传感器把从核电厂
收稿日期：2020-09-25
作者简介：兰林（1996-），男，四川南充人，硕士，研究方向：安全级DCS技术研究与应用。
DOI:10.3969/j.issn.1671-1041.2020.11.014
文章编号：1671-1041(2020)11-0052-05
现场采集来的数据上传至控制器中，经控制算法软件处理后输出，从而控制核电厂现场执行器的安全动作。因此，控制算法软件的安全性、可信性直接关系着核电厂运行的安全性、稳定性。传统的控制算法编写多采用手工编码的
兰 林·核安全级DCS系统模型驱动可信代码自动生成方法
第11期53
方式，此方法对于仪控工程师的编码能力要求较高，由于
在编码过程中容易引入错误，因而需要对编写的代码进行
大量的单元测试、集成调试以保证代码的正确性和安全
性，占用了仪控工程师大量的时间和精力。为解决当前
手工编码存在的问题，高安全性的应用程序开发环境
（Safety-Critical Application Development Environment，简称
SCADE）[1,2]提出了模型驱动代码自动生成的一种全新的控
制算法软件设计的思路。SCADE是法国Esterel Technologies
公司研制的比较成熟的高安全性应用程序开发环境，主要
用于开发满足DO-178B标准的嵌入式软件[3,4]，广泛用于
嵌入式安全攸关领域，如核电、轨道交通、国防等。目前，
国内核电DCS系统控制领域还没有一个类似于SCADE的
高安全程序开发环境，为改变高安全性的控制算法软件开
发环境完全依赖进口的局面，结合核电厂安全级DCS系统
控制需求，研制一种适用于核电厂安全级DCS系统算法软
件设计的、由模型驱动的代码自动生成的综合性建模环境。
基于数据流图和有限状态机方法，开发了图形化建模软件，
用于仪控工程师通过拖拽功能图符块编写控制算法；XML
文件信息提取软件，用于把图符块对应的XML文件转化为
Lustre程序的形式；基于形式化验证技术，开发了可信代码
生成软件，用于把Lustre程序转化为安全、正确的C程序。
最后，将这些软件集成在一起使用，为核安全级DCS系统控制算法开发提供了一个由图形化算法模型驱动代码自动生成的解决方案。本文将针对图形化建模软件、XML文件信息提取方法和可信代码生成软件进行详细介绍。
1  图形化建模软件
图形化建模是核安全级DCS系统控制算法开发过程中的重要环节，为核安全级DCS系统模型驱动代码自动生成方法提供算法模型。在充分研究核电厂DCS系统对象物理特性、结构特性、行为特性的基础上，将NASPIC平台系统的设备（包括板卡、机箱、机柜）、变量（包括模拟量、数字量类型等）、核电厂控制算法功能块抽象为对应的图形化的设备模型、变量模型和算法模型，它们分别用于创建虚拟硬件设备及其连接关系、通道绑定与通道配置、创建输入信号的运算逻辑。如图1所示，在图形化建模界面软件中，通过拖拽模型来创建系统控制算法。以下将分别介绍图形化设备建模、变量建模和算法建模。
1.1  设备建模
设备建模主要负责创建硬件设备模型和硬件设备之间的映射关系，首先根据核电厂实际工程控制需要，创建机柜模型、机箱模型、板卡模型以及通道模型，为进行变量建模提供设备通道以及设备间的连接关
系。设备建模提供了丰富的设备库，并根据当前建模所处阶段，自动增减设备库中可选硬件设备，这一设计提升了设备建模过程的便利性，同时也降低了误操作的概率。设备建模包括：①机柜建模。根据机柜类型、机柜容量等信息创建机柜模型，用于搭建机柜集，初步建立控制系统框架；②机箱建模。由机柜配置信息创建机箱模型，机箱模型作为板卡模型的容器，主要是将执行控制功能的板卡进行逻辑组合；③板卡建模。板卡是实现具体控制功能的硬件集成电路板卡，包括DO、AO、AI、DI等10余种类型，仪控工程师可根据系统数据采集任务需求来创建板卡模型，根据制定的建模规则在机箱相应的槽号插入板卡，可满足多样化和定制化的系统控制功能需求；④通道建模。通道在建模过程中可以通常和变量建模同步进行，底层设备的参数信息通过通道的变量模型信息展示和传输，同时通道用于建立两个或多个机箱之间的通信。
1.2  变量建模
变量建模主要用于创建物理通道与虚拟通道的映射关系，配置通道属性（如数据采集量程、通道安全行为、预设值等），创建设备间通信的网络参数配置等。变量建模的前提是存在设备模型，即虚拟通道必须建立在物理通道之上，同时变量模型为后续的算法建模提供变量信息，用于关联算法功能图符块。变量模型是整个控制系统的基本组成单元，具有属性繁多、规则复杂等特点，其正确性直接影响控制系统的输入、输出的正确性。变量模型研究的关键在于建立覆盖变量所有属性、所有行为规则的模型检查机制，包括检查预期的特定属性是否存在；预期的属性是否已填值；预期的属性值是否落在条件范围内；
网络路由关系是否正确等，保证了建模的正确性和安全性。
1.3  算法建模
算法建模是核安全DCS系统控制算法设计的核心，是
图1  图形建模结构示意图
Fig.1  Schematic diagram of graphical modeling structure
第27卷54仪器仪表用户INSTRUMENTATION
基于形式化验证的可信代码生成的基础。算法建模基于数
据流图和有限状态机方法，分别对连续系统和离散系统进
行建模，模型具有严格的数学语义，保证了算法模型的设
计与需求具有一致性。其中，数据流图用于连续系统建
模，描述了数据的处理过程、反应时序及因果关系，通过
仪控工程师定义的输入变量接收核电厂现场采集的控制信
号，经过图形化控制算法模型处理后，再输出给DO模块，
控制核电厂现场执行器的安全动作。数据流图建模中最基
本的功能单元是节点，类似于C语言中的函数，并且提供算术运算、逻辑运算、比较运算、时间运算等
基本运算符，利用这些预定义的运算符及自定义的节点，可继续构建新的、更复杂的节点，以完成更复杂的功能。这两种建模方式既可单独使用也可结合使用，满足了核电厂DCS系统多样化的控制需求，大大提高了设计效率。
2  XML文件数据提取
在图形化建模软件中，仪控工程师根据工程实际控制需求进行图形化控制算法建模后，源程序以XML格式文件存在。工程的XML文件包含当前工程中用到的组合逻辑块XML文件、工程配置XML文件、预定义XML文件以及算法块XML文件。为了简化可信代码生成器的构造和证明，在把图形化控制算法模型转化为可信代码之前，用一种中间语言来表示图形化算法模型，即把XML中的控制算法信息提取成Lustre程序。XML格式文件中的信息结构如图2所示，包括以下几部分：①工程信息描述区域，主要存储工程的基本信息；②输入参数、输出参数、局部变量描述区域，主要存储从现场采集到的待处理的数据、局部变量数据以及输出的结果；③控制算法描述区域，主要存储处理输入数据的算法；④图形化数据区，主要存储图形化控制算法软件的算法图符块的几何信息。
Lustre是一种同步数据流语言[5]，一个Lustre程序是由多个node构成，node相当于C语言中的一个函数，不同点在于其输入参数和输出参数是一个流（Stream），源源不断地处理从控制现场采集到的数据，node的基本结构如图3所示，其中node、returns、var、let、tel为Lustre程序的关键字。在XML文件
数据提取过程中，XML文件数据提取软件首先加载工程配置XML文件，获取到所有的组合逻辑块XML文件、预定义XML文件、算法包XML文件中的算法逻辑块的文件地址，再将文件地址存储起来，随后依据XML文件数据提取软件的执行流程，来解析所有的XML文件。XML文件数据解析的基本流程如图4所示，读取到XML文件中数据的开始标签<start>，进入此标签的数据存储结构，对标签内的数据进行数据的映射，包括读到<inputs>标签时，把数据存储至node的输入参数；<outputs>标签，把数据存储至node的输出参数；<locals>标签，把数据存储至node的局部变量；<data>标签，把数据存储至node的控制算法区，当读取到结束标签<start>，
图2  XML文件数据结构图
Fig.2  XML File data structure diagram
图3  Lustre代码基本结构
Fig.3  Basic structure of Lustre code
图4  XML文件信息提取过程
Fig.4  XML File information extraction process
则完成了这个XML文件信息的提取，循环读取工程的其他XML文件信息。最终，实现了把一个工程的XML文件解析成了一个Lustre程序。
3  可信代码自动生成软件设计
在基于形式化验证技术的可信代码生成领域，常用的方法包括：翻译验证（translation validation）[6-8]，它是一种等价性验证方式，是一种轻量级形式化验证技术，不需要
兰 林·核安全级DCS系统模型驱动可信代码自动生成方法
第11期55
图5  可信代码生成软件架构图
Fig.5  Software architecture diagram of trusted
code generation
对代码生成软件本身进行验证，核心在于构造一个翻译验证器；定理证明[9,10]，这是一种重量级形式化验证技术，是最严格的验证方式，其对代码生成过程本身进行证明，可保证代码生成过程的正确性，最著名的代表作是CompCert 编译器[11-14]。为解决图形化模型转化为C 程序过程中可能存在的误编译问题，基于前人成功的经验，在可信代码生成软件的开发过程中，引入形式化验证技术——定理证明，通过对代码生成过程的正确性进行验证，保证源语言与目标语言语义的一致性，进而保证代码生成过程的正确性。如图5所示，为可信代码生成软件的形式化开发架构图。总共包括4层：
1）形式化规范描述层：研究了可信代码生成软件的功能需求和安全属性需求，并在辅助定理证明工具Coq [15]中将其转换为形式化规范描述。如图5所示，为了简化证明框架和满足代码生成软件的功能需求，引入了7种中间建模语言将整个代码转换过程拆分成8个翻译阶段，对这些中间建模语言的控制语句、时态算子、高阶算子的行为、状态转换以及安全属性等使用操作语义[16-18]进行规范描述，得到其动态语义模型。在此基础上，可开发语义一致性的性质、定理，进而对翻译过程的语义一致性进行验证，这是形式化逻辑验证层的基础。
2）形式化逻辑验证层：图5中双箭头表示对形式化规范描述层中定义的安全属性和语义一致性进行验证，
经过逻辑推理证明成功后，代码生成过程中翻译前后语义具有一致性且满足定义的安全属性。在逻辑验证过程中，为解决验证工作的可复用性差等问题，创造性地提出“小步验证”和“反向验证”的方法。“小步验证”基于7种中间建模语言将整个翻译过程拆分为多个“小步”，每步只完成固定验证任务，降低了证明过程的难度。“反向验证”是由通常的从前往后按顺序验证，转变为从后往前的验证方式，其目地是保证所做的证明过程完成后，不会因为后续的证明过程出现错误而推翻已证明的内容。
3）验证后算法抽取层：验证后的可信算法抽取采用辅助定理证明工具Coq 完成，在Coq 中编写的翻译算法通常是可以用常规函数式程序设计语言实现的函数模型。通过Coq 的抽取机制（Extraction），在可信代码生成软件开发过程中，把逻辑验证成功后的翻译算法中的每个函数自动映射到OCaml 语言中对应的函数，经二次编译后，得到可信代码生成软件的可运行程序。在Coq 中开发的翻译算法如实地描述了抽取出的算法的行为，满足在形式化开发中描述的规范说明，并且在逻辑验证层对算法的证明进行了逻辑证明，故Coq 抽取出的每个算法都是可信的，进而保证了可信代码生成软件的安全性和可信性。
4）可信代码生成软件应用层：图形化的算法模型经XML 文件信息提取成Lustre 程序后，经可信代码生成软件的处理后生成可信的C 程序。
基于形式化验证技术的可信代码生成软件是基于严格
的数学理论和形式化方法，其代码生成的正确性和安全性经过严格数学推理证明，可免去代码单元测试
环节，进而有效缩短了验证时间和提升了建模效率。
4  软件集成使用
目前，仪控工程师通过图形化建模软件NASPES 来开发图形化控制算法，然后通过调用SCADE KCG 把它转化C 程序，然后把得到的C 程序下装到NASPIC 平台中，最后经二次编译后，生成可执行代码在控制器中运行。基于本文的研究，实现了XML 文件数据提取软件和可信代码生成工具后，可完全替换代码生成工具KCG，实现NASPIC 平台的完全国产化。由于在可信代码生成工具的开发过程中，除了使用V&V 和测试的手段来保证其可信性，还采用形式化验证方法对代码生成器的开发过程进行正确性的验证。因此，生成的代码的可信性在理论上超过KCG。
把图形化建模软件、XML 文件数据提取软件和可信代码生成软件集成后使用。如图6所示，仪控工程师通过在图形化建模软件中拖拽算法图符块来创建控制算法，然后调用XML 文件信息提取软件把图形化控制算法对应的XML 文件数据转化为Lustre 程序，然后调用可信代码生成软件把生成的Lustre 程序转化为可信C 代码，最后经二次编译后下装到核安全级DCS 平台，控制核电厂的安全、可靠地运行。
5  结束语
本文针对核安全级DCS 系统控制算法开发环境完全依赖国外进口的现状，基于图形化建模技术、XML
文件解析技术和形式化验证技术，提出了一种适用于核安全级DCS 系统的、由模型驱动代码自动生成的控制算法设计方法。
图形化控制算法设计降低了对仪控工程师的编码能力要求，
第27卷
56  仪器仪表用户INSTRUMENTATION 图6  模型驱动代码自动生成流程图
Fig.6  Flow chart of model-driven code automatic generation
摆脱了传统“手工编码”设计控制算法的方式，把控制算法开发人员从易出错的编码语义、语法设计和反复的代码验证等繁复的工作中解放出来，更专注于核安全级DCS 系统控制算法设计本身，从而提高控制算法设计效率，保证算法的可信性；形式化验证技术用于可信代码生成软件的开发，保证了图形化算法模型转化成正确的目标C 程序，可完成在NASPIC 平台中对代码生成工具KCG 的替换。完成NASPIC 平台中的代码生成器KCG 的替换具有重要的意义，一方面，可避免由于KCG 代码黑盒带来的安全隐患，提高DCS 系统安全性；另一方面，将摆脱核电关键建模软件受制于人的境地，实现NASPIC 平台的完全自主化。
参考文献：
Pierre Mattei A L, Marques d C A, Vieria Dias L A, et
al. Nanosatellite Event Simulator Development Using
Scrum Agile Method and Safety-Critical Application Development Environment[C].International Conference on Information Technology-New Generations.IEEE Computer Society,2015:101-106.
J oshi A, Heimdahl M P E. Model-Based Safety Analysis
of Simulink Models Using SCADE Design Verifier[C].
International Conference on Computer Safety, Reliability and Security.2005:122-135.
刘晶晶，刘增明.基于SCADE的嵌入式软件开发[J].微处理机,2013(01):36-39.
Mikáč, Jan, Caspi, Paul. Flush: a system development tool based on scade/lustre[J].Fmics,2005,8(6):27-34.
Caspi P , Pilaud D , Halbwachs N , et al. LUSTRE: a declarative language for real-time programming[C].Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages.ACM,1987.
reactor technology
Pnueli A .Translation validation[C].International Conference on Tools & Algorithms for the Construction & Analysis of Systems. Springer Berlin Heidelberg,1998.
Li A P. Translation Validation: From SIGNAL to C[M].1999.
Pnueli A . Translation validation[C].International Conference on Tools &Algorithms for the Construction & Analysis of Systems. Springer Berlin Heidelberg,1998.
John Mccarthy J P . Correctness of a compiler for arithmetic expressions[J]. Proc. Sympos.Appl.Math.Vol.XIX,1967:33-41.
Yonezawa A , Hale R . Proving Compiler Correctness in a Mechanized Logic R. Milner and R. Weyhrauch[J].Information and Control,1974,26(4):396-397.
Leroy X . Formal verification of a realistic compiler[M].ACM,2009.
Blazy S , Leroy X . Mechanized Semantics for the Clight Subset of t h e  C  L a n g u a g e [J ].J o u r n a l  o f  A u t o m a t e d Reasoning,2009,43(3):263-288.
Leroy X . Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[J].Acm Sigplan Notices,2006,41(1):42-54.
Leroy X . A formally verified compiler back-end[J].Journal of Automated Reasoning,2009,43(4):363.
Coq development team. The Coq proof assistant[EB/OL].coq.inria.fr.
Christine Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq[J]. From Semantics to Computer Science,2009:383-413.
Plotkin G D . A Structural Approach to Operational Semantics[J].Journal of Logic & Algebraic Programming,2004,60-61:17-139.Plotkin G D . The origins of structural operational semantics[J]. Journal of Logic & Algebraic Programming,2004,60-61(none):3-15.
[1][2][3][4][5]
[6]
[7][8]
[9]
[10]
[11][12][13][14][15][16][17][18]
（上接第7页）
参考文献：
任元会.工业与民用配电设计手册[M].北京：中国电力出版
社,2005.
输变电设备故障诊断与事故处理实用手册编委会.输变电设备
故障诊断与事故处理实用手册[M].北京：北京银冠电子出版有限公司,2001.
赵家礼.电动机修理手册[M].北京：机械工业出版社,1988.
[1][2]
[3]

版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。