Scade 6 编译原理的参考实现 - LustreC

Scade 6建模语言的编译原理基础在SCADE Suite v6于2008年发布的同年，在LCTES’08[Bie08]中发表。LCTES'08 中描述的编译机制，随后成为一些Lustre编译器的参考原理，比如Velus[Brun20]、Heptagon[Leonard13]、LustreC[LustreC]等。这里将对LustreC进行介绍。

LustreC编译器的架构围绕着于2008年在LCTES会议上提出的模块化编译方案构建。它是一款具备验证功能的开源Lustre语言编译器，目前主要通过CocoSim平台投入使用 —— 该平台是一款用于对Simulink模型执行验证与确认（V&V）的Matlab工具箱。在CocoSim内部，Lustre语言被用作中间表示（注：指编译过程中用于连接源代码与目标代码的中间代码形式），其生成代码或验证产物的功能主要依赖于LustreC编译器来实现。

背景补充: CocoSim

对CocoSim[CocoSim], CoCoSim是一款可从Matlab Simulink环境中直接调用的工具箱（功能类似Simulink Design Verifier）。该工具既可用于代码生成（例如生成C语言、Rust语言或Lustre语言代码），也可用于属性验证。其前端会执行一系列预处理操作（即把不同的Simulink模块转化为基础模块）以及优化操作。

预处理后的Simulink模型将作为编译器的输入。编译器对预处理后的Simulink模型进行模块化转换，并生成Lustre代码。此外，它还会对各种Simulink/Stateflow结构（如信号名称、模块类型等）进行记录。这使得在Lustre程序中能够追踪Simulink/Stateflow的结构。

生成的Lustre模型将作为外部Solver的输入。外部输入接收Lustre代码，并执行以下两种操作之一：(i) 将其编译为命令式代码（C语言或Rust语言）；(ii) 对所提供的属性进行安全性分析。在编译方面，它使用LustreC；而在安全性验证方面，它使用Zustre、Kind2或JKind中的一种工具。安全性分析的结果会反馈到Matlab环境中。如果所提供的属性被证伪，CoCoSim会提供在Matlab环境中模拟反例轨迹的方法。

[Bie08]: Clock-directed Modular Code Generation for Synchronous Data-flow Languages
[Brun20]: 参考Lelio Brun的博士论文
[Leonard13]: 参考Leonard Gerard的博士论文
[LustreC]: gitlab.isae-supaero.fr/lustrec/lustrec-public-version
[CocoSim]: github.com/NASA-SW-VnV/CoCoSim