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

相关文章

Oracle查询优化之高效实现仅查询前10条记录的方法与实践

《Oracle查询优化之高效实现仅查询前10条记录的方法与实践》:本文主要介绍Oracle查询优化之高效实现仅查询前10条记录的相关资料,包括使用ROWNUM、ROW_NUMBER()函数、FET... 目录1. 使用 ROWNUM 查询2. 使用 ROW_NUMBER() 函数3. 使用 FETCH FI

Python脚本实现自动删除C盘临时文件夹

《Python脚本实现自动删除C盘临时文件夹》在日常使用电脑的过程中,临时文件夹往往会积累大量的无用数据,占用宝贵的磁盘空间,下面我们就来看看Python如何通过脚本实现自动删除C盘临时文件夹吧... 目录一、准备工作二、python脚本编写三、脚本解析四、运行脚本五、案例演示六、注意事项七、总结在日常使用

Java实现Excel与HTML互转

《Java实现Excel与HTML互转》Excel是一种电子表格格式,而HTM则是一种用于创建网页的标记语言,虽然两者在用途上存在差异,但有时我们需要将数据从一种格式转换为另一种格式,下面我们就来看看... Excel是一种电子表格格式,广泛用于数据处理和分析,而HTM则是一种用于创建网页的标记语言。虽然两

Java中Springboot集成Kafka实现消息发送和接收功能

《Java中Springboot集成Kafka实现消息发送和接收功能》Kafka是一个高吞吐量的分布式发布-订阅消息系统,主要用于处理大规模数据流,它由生产者、消费者、主题、分区和代理等组件构成,Ka... 目录一、Kafka 简介二、Kafka 功能三、POM依赖四、配置文件五、生产者六、消费者一、Kaf

使用Python实现在Word中添加或删除超链接

《使用Python实现在Word中添加或删除超链接》在Word文档中,超链接是一种将文本或图像连接到其他文档、网页或同一文档中不同部分的功能,本文将为大家介绍一下Python如何实现在Word中添加或... 在Word文档中,超链接是一种将文本或图像连接到其他文档、网页或同一文档中不同部分的功能。通过添加超

windos server2022里的DFS配置的实现

《windosserver2022里的DFS配置的实现》DFS是WindowsServer操作系统提供的一种功能,用于在多台服务器上集中管理共享文件夹和文件的分布式存储解决方案,本文就来介绍一下wi... 目录什么是DFS?优势:应用场景:DFS配置步骤什么是DFS?DFS指的是分布式文件系统(Distr

NFS实现多服务器文件的共享的方法步骤

《NFS实现多服务器文件的共享的方法步骤》NFS允许网络中的计算机之间共享资源,客户端可以透明地读写远端NFS服务器上的文件,本文就来介绍一下NFS实现多服务器文件的共享的方法步骤,感兴趣的可以了解一... 目录一、简介二、部署1、准备1、服务端和客户端:安装nfs-utils2、服务端:创建共享目录3、服

C#使用yield关键字实现提升迭代性能与效率

《C#使用yield关键字实现提升迭代性能与效率》yield关键字在C#中简化了数据迭代的方式,实现了按需生成数据,自动维护迭代状态,本文主要来聊聊如何使用yield关键字实现提升迭代性能与效率,感兴... 目录前言传统迭代和yield迭代方式对比yield延迟加载按需获取数据yield break显式示迭

Python实现高效地读写大型文件

《Python实现高效地读写大型文件》Python如何读写的是大型文件,有没有什么方法来提高效率呢,这篇文章就来和大家聊聊如何在Python中高效地读写大型文件,需要的可以了解下... 目录一、逐行读取大型文件二、分块读取大型文件三、使用 mmap 模块进行内存映射文件操作(适用于大文件)四、使用 pand

python实现pdf转word和excel的示例代码

《python实现pdf转word和excel的示例代码》本文主要介绍了python实现pdf转word和excel的示例代码,文中通过示例代码介绍的非常详细,对大家的学习或者工作具有一定的参考学习价... 目录一、引言二、python编程1,PDF转Word2,PDF转Excel三、前端页面效果展示总结一