Lustre 代码生成器 - 中国核动力研究设计院(核动力院)NASCG 实现

本文主要是介绍Lustre 代码生成器 - 中国核动力研究设计院(核动力院)NASCG 实现,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

本文的详细信息可参考 兰林 - 《应用于核安全级DCS系统的代码生成器的设计和实现》(2020.12)。

Lustre 同步数据流语言提供了对实时控制系统(real-time control system)提供了"同步假设"计算模型的编程语言抽象。由于实时控制系统往往是安全攸关系统(safety-critical system),因此,在产业界此类技术被应用于如核电、航空、轨交等领域。安全关键应用开发环境套件(SCADE Suite)背后的技术基础,在历史发展上,也受 Lustre 语言很深的影响。

虽然 Lustre 是法式技术,但在国内也有 Lustre 编译器的工作。如文本提到的中国核动力研究设计院(核动力院, NPIC)研发的 NASCG,即为 Lustre 编译器的一个实现。由于使同步语言在产业界取得最大成功的 SCADE Suite 产品中,同步语言编译器被命名为“代码生成器”(KCG, qualified code generator),因此,Lustre 编译器在命名上也被称为 Lustre 代码生成器。

NASCG 的输入为 Lustre 文本语言,输出为 C 程序语言。在程序架构上,遵循了常规的编译器架构:

  • 词法分析
  • 语法分析
  • 语义分析
  • 中间代码生成
  • 代码翻译

NASCG 在实现技术选择上,由于其特色为在语义分析中采用定理证明形式化技术(Coq),因此,采用了 OCaml 作为实现的编程语言。对词法分析,采用了 OCaml lex;对语法分析,采用了 OCaml yacc;对语义检查与翻译算法,采用 Coq 编写,并且抽取为 OCaml 程序。

对实现中部分的详细实现机制,可参考兰林 - 《应用于核安全级DCS系统的代码生成器的设计和实现》(2020.12)

这篇关于Lustre 代码生成器 - 中国核动力研究设计院(核动力院)NASCG 实现的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/981466

相关文章

Vue项目的甘特图组件之dhtmlx-gantt使用教程和实现效果展示(推荐)

《Vue项目的甘特图组件之dhtmlx-gantt使用教程和实现效果展示(推荐)》文章介绍了如何使用dhtmlx-gantt组件来实现公司的甘特图需求,并提供了一个简单的Vue组件示例,文章还分享了一... 目录一、首先 npm 安装插件二、创建一个vue组件三、业务页面内 引用自定义组件:四、dhtmlx

Vue ElementUI中Upload组件批量上传的实现代码

《VueElementUI中Upload组件批量上传的实现代码》ElementUI中Upload组件批量上传通过获取upload组件的DOM、文件、上传地址和数据,封装uploadFiles方法,使... ElementUI中Upload组件如何批量上传首先就是upload组件 <el-upl

Docker部署Jenkins持续集成(CI)工具的实现

《Docker部署Jenkins持续集成(CI)工具的实现》Jenkins是一个流行的开源自动化工具,广泛应用于持续集成(CI)和持续交付(CD)的环境中,本文介绍了使用Docker部署Jenkins... 目录前言一、准备工作二、设置变量和目录结构三、配置 docker 权限和网络四、启动 Jenkins

Python3脚本实现Excel与TXT的智能转换

《Python3脚本实现Excel与TXT的智能转换》在数据处理的日常工作中,我们经常需要将Excel中的结构化数据转换为其他格式,本文将使用Python3实现Excel与TXT的智能转换,需要的可以... 目录场景应用:为什么需要这种转换技术解析:代码实现详解核心代码展示改进点说明实战演练:从Excel到

如何使用CSS3实现波浪式图片墙

《如何使用CSS3实现波浪式图片墙》:本文主要介绍了如何使用CSS3的transform属性和动画技巧实现波浪式图片墙,通过设置图片的垂直偏移量,并使用动画使其周期性地改变位置,可以创建出动态且具有波浪效果的图片墙,同时,还强调了响应式设计的重要性,以确保图片墙在不同设备上都能良好显示,详细内容请阅读本文,希望能对你有所帮助...

C# string转unicode字符的实现

《C#string转unicode字符的实现》本文主要介绍了C#string转unicode字符的实现,文中通过示例代码介绍的非常详细,对大家的学习或者工作具有一定的参考学习价值,需要的朋友们下面随... 目录1. 获取字符串中每个字符的 Unicode 值示例代码:输出:2. 将 Unicode 值格式化

python安装whl包并解决依赖关系的实现

《python安装whl包并解决依赖关系的实现》本文主要介绍了python安装whl包并解决依赖关系的实现,文中通过图文示例介绍的非常详细,对大家的学习或者工作具有一定的参考学习价值,需要的朋友们下面... 目录一、什么是whl文件?二、我们为什么需要使用whl文件来安装python库?三、我们应该去哪儿下

Python脚本实现图片文件批量命名

《Python脚本实现图片文件批量命名》这篇文章主要为大家详细介绍了一个用python第三方库pillow写的批量处理图片命名的脚本,文中的示例代码讲解详细,感兴趣的小伙伴可以了解下... 目录前言源码批量处理图片尺寸脚本源码GUI界面源码打包成.exe可执行文件前言本文介绍一个用python第三方库pi

Java中将异步调用转为同步的五种实现方法

《Java中将异步调用转为同步的五种实现方法》本文介绍了将异步调用转为同步阻塞模式的五种方法:wait/notify、ReentrantLock+Condition、Future、CountDownL... 目录异步与同步的核心区别方法一:使用wait/notify + synchronized代码示例关键

Nginx实现动态封禁IP的步骤指南

《Nginx实现动态封禁IP的步骤指南》在日常的生产环境中,网站可能会遭遇恶意请求、DDoS攻击或其他有害的访问行为,为了应对这些情况,动态封禁IP是一项十分重要的安全策略,本篇博客将介绍如何通过NG... 目录1、简述2、实现方式3、使用 fail2ban 动态封禁3.1 安装 fail2ban3.2 配